From a07f67f6f1deba8b14672c618c003ec345d7970a Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 24 Sep 2016 16:37:04 +0200
Subject: 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".
---
 test-suite/bugs/closed/5097.v | 7 +++++++
 1 file changed, 7 insertions(+)
 create mode 100644 test-suite/bugs/closed/5097.v

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/5097.v b/test-suite/bugs/closed/5097.v
new file mode 100644
index 0000000000..37b239cf61
--- /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.
-- 
cgit v1.2.3