blob: 5daaf9edbfde343692e03b3516b0dae5f26221cc (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
|
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.
|
