blob: 37b239cf61ca704fa403ba0ae63911fd42934e28 (
plain)
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.
|