diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-09-24 16:37:04 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-10-20 20:22:07 +0200 |
| commit | a07f67f6f1deba8b14672c618c003ec345d7970a (patch) | |
| tree | c9f33707c6c7dc3fae71d1e0a7e35e5686751a5d /test-suite/bugs/closed/5097.v | |
| parent | 317ae3b327d201530730ed2cce5f44e8763814d4 (diff) | |
A fix for #5097 (status of evars refined by "clear" in ltac: closed wrt evars).
If an existing evar was cleared in pretyping (typically while
processing "ltac:"), it created an evar considered as new. Updating
them instead along the "cleared" flag.
If correct, I suspect similar treatment should be done for refining
along "change", "rename" and "move".
Diffstat (limited to 'test-suite/bugs/closed/5097.v')
| -rw-r--r-- | test-suite/bugs/closed/5097.v | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/5097.v b/test-suite/bugs/closed/5097.v new file mode 100644 index 000000000..37b239cf6 --- /dev/null +++ b/test-suite/bugs/closed/5097.v @@ -0,0 +1,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. |