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
|
Require Import TestSuite.admit.
(* Check that Goal.hyps and Goal.env are consistent *)
(* This is a shorten variant of the initial bug which raised anomaly *)
Goal forall x : nat, (forall z, (exists y:nat, z = y) -> True) -> True.
evar nat.
intros x H.
apply (H n).
unfold n. clear n.
eexists.
reflexivity.
Unshelve.
admit.
Admitted.
(* Alternative variant which failed but without raising anomaly *)
Goal forall x : nat, True.
evar nat.
intro x.
evar nat.
assert (H := eq_refl : n0 = n).
clearbody n n0.
exact I.
Unshelve.
admit.
Admitted.
|
