aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/failure/evarclear2.v
blob: 0f7768112b7e53f12f3d5ec9446b95694074d9a9 (plain)
1
2
3
4
5
6
7
8
9
Set Printing Existential Instances.
Set Printing All.
Goal let y:=0 in exists x:y=y, x = x.
intros.
eexists.
rename y into z.
unfold z at 1 2.
(* should fail because the evar type depends on z *)
Fail clear z.