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".

1 files changed, 22 insertions, 0 deletions

diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 759e0e4d6d..9a9c946aeb 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -600,6 +600,28 @@ let gather_dependent_evars evm l =
 
 (* /spiwack *)
 
+(** [advance sigma g] returns [Some g'] if [g'] is undefined and is
+    the current avatar of [g] (for instance [g] was changed by [clear]
+    into [g']). It returns [None] if [g] has been (partially)
+    solved. *)
+(* spiwack: [advance] is probably performance critical, and the good
+   behaviour of its definition may depend sensitively to the actual
+   definition of [Evd.find]. Currently, [Evd.find] starts looking for
+   a value in the heap of undefined variable, which is small. Hence in
+   the most common case, where [advance] is applied to an unsolved
+   goal ([advance] is used to figure if a side effect has modified the
+   goal) it terminates quickly. *)
+let rec advance sigma evk =
+  let evi = Evd.find sigma evk in
+  match evi.evar_body with
+  | Evar_empty -> Some evk
+  | Evar_defined v ->
+      if Option.default false (Store.get evi.evar_extra cleared) then
+        let (evk,_) = Term.destEvar v in
+        advance sigma evk
+      else
+        None
+
 (** The following functions return the set of undefined evars
     contained in the object, the defined evars being traversed.
     This is roughly a combination of the previous functions and