Quelle  bug_2969.v

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.