products/sources/formale sprachen/Coq/dev/ci/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: bug_5255.v   Sprache: Unknown

Section foo.
  Context (x := 1).
  Definition foo : x = 1 := eq_refl.
End foo.

Module Type Foo.
  Context (x := 1).
  Definition foo : x = 1 := eq_refl.
End Foo.

Set Universe Polymorphism.

Inductive unit := tt.
Inductive eq {A} (x y : A) : Type := eq_refl : eq x y.

Section bar.
  Context (x := tt).
  Definition bar : eq x tt := eq_refl _ _.
End bar.

Module Type Bar.
  Context (x := tt).
  Definition bar : eq x tt := eq_refl _ _.
End Bar.

[ Dauer der Verarbeitung: 0.16 Sekunden  (vorverarbeitet)  ]