1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
|
Module A.
Set Primitive Projections.
Record hSet : Type := BuildhSet { setT : Type; iss : True }.
Ltac head_hnf_under_binders x :=
match eval hnf in x with
| ?f _ => head_hnf_under_binders f
| (fun y => ?f y) => head_hnf_under_binders f
| ?y => y
end.
Goal forall s : hSet, True.
intros.
let x := head_hnf_under_binders setT in pose x.
set (foo := eq_refl (@setT )). generalize foo. simpl. cbn.
Abort.
End A.
Module A'.
Set Universe Polymorphism.
Set Primitive Projections.
Record hSet (A : Type) : Type := BuildhSet { setT : Type; iss : True }.
Ltac head_hnf_under_binders x :=
match eval compute in x with
| ?f _ => head_hnf_under_binders f
| (fun y => ?f y) => head_hnf_under_binders f
| ?y => y
end.
Goal forall s : @hSet nat, True.
intros.
let x := head_hnf_under_binders setT in pose x.
set (foo := eq_refl (@setT nat)). generalize foo. simpl. cbn.
Abort.
End A'.
|
