test-suite/bugs/closed/5097.v


1
2
3
4
5
6
7

(* Tracing existing evars along the weakening rule ("clear") *)
Goal forall y, exists x, x=0->x=y.
intros.
eexists ?[x].
intros.
let x:=constr:(ltac:(clear y; exact 0)) in idtac x.
Abort.