Merge PR #1102: On the detection of evars which "advanced" (and a fix to BZ#5757)

4 files changed, 17 insertions, 21 deletions

diff --git a/engine/evarutil.ml b/engine/evarutil.ml
index 339c6a248e..eabfb7b398 100644
--- a/engine/evarutil.ml
+++ b/engine/evarutil.ml
@@ -478,8 +478,6 @@ type clear_dependency_error =
 
 exception ClearDependencyError of Id.t * clear_dependency_error
 
-let cleared = Store.field ()
-
 exception Depends of Id.t
 
 let rec check_and_clear_in_constr env evdref err ids global c =
@@ -552,13 +550,6 @@ let rec check_and_clear_in_constr env evdref err ids global c =
               let evd = !evdref in
               let (evd,_) = restrict_evar evd evk filter None in
               evdref := evd;
-	    (* spiwack: hacking session to mark the old [evk] as having been "cleared" *)
-	      let evi = Evd.find !evdref evk in
-	      let extra = evi.evar_extra in
-	      let extra' = Store.set extra cleared true in
-	      let evi' = { evi with evar_extra = extra' } in
-	      evdref := Evd.add !evdref evk evi' ;
-	    (* spiwack: /hacking session *)
               Evd.existential_value !evdref ev
 
       | _ -> map_constr (check_and_clear_in_constr env evdref err ids global) c
@@ -665,11 +656,9 @@ let rec advance sigma evk =
   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
+      match is_restricted_evar evi with
+      | Some evk -> advance sigma evk
+      | None -> None
 
 (** The following functions return the set of undefined evars
     contained in the object, the defined evars being traversed.
diff --git a/engine/evarutil.mli b/engine/evarutil.mli
index 14173e774d..ee0fae3d46 100644
--- a/engine/evarutil.mli
+++ b/engine/evarutil.mli
@@ -204,10 +204,6 @@ type clear_dependency_error =
 
 exception ClearDependencyError of Id.t * clear_dependency_error
 
-(* spiwack: marks an evar that has been "defined" by clear.
-    used by [Goal] and (indirectly) [Proofview] to handle the clear tactic gracefully*)
-val cleared : bool Store.field
-
 val clear_hyps_in_evi : env -> evar_map ref -> named_context_val -> types ->
   Id.Set.t -> named_context_val * types
 
diff --git a/engine/evd.ml b/engine/evd.ml
index f1b5419dec..324f883e8e 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -630,7 +630,9 @@ let evar_source evk d = (find d evk).evar_source
 let evar_ident evk evd = EvNames.ident evk evd.evar_names
 let evar_key id evd = EvNames.key id evd.evar_names
 
-let define_aux def undef evk body =
+let restricted = Store.field ()
+
+let define_aux ?dorestrict def undef evk body =
   let oldinfo =
     try EvMap.find evk undef
     with Not_found ->
@@ -640,7 +642,10 @@ let define_aux def undef evk body =
         anomaly ~label:"Evd.define" (Pp.str "cannot define undeclared evar.")
   in
   let () = assert (oldinfo.evar_body == Evar_empty) in
-  let newinfo = { oldinfo with evar_body = Evar_defined body } in
+  let evar_extra = match dorestrict with
+    | Some evk' -> Store.set oldinfo.evar_extra restricted evk'
+    | None -> oldinfo.evar_extra in
+  let newinfo = { oldinfo with evar_body = Evar_defined body; evar_extra } in
   EvMap.add evk newinfo def, EvMap.remove evk undef
 
 (* define the existential of section path sp as the constr body *)
@@ -653,6 +658,9 @@ let define evk body evd =
   let evar_names = EvNames.remove_name_defined evk evd.evar_names in
   { evd with defn_evars; undf_evars; last_mods; evar_names }
 
+let is_restricted_evar evi =
+  Store.get evi.evar_extra restricted
+
 let restrict evk filter ?candidates ?src evd =
   let evk' = new_untyped_evar () in
   let evar_info = EvMap.find evk evd.undf_evars in
@@ -667,7 +675,7 @@ let restrict evk filter ?candidates ?src evd =
   let ctxt = Filter.filter_list filter (evar_context evar_info) in
   let id_inst = Array.map_of_list (NamedDecl.get_id %> mkVar) ctxt in
   let body = mkEvar(evk',id_inst) in
-  let (defn_evars, undf_evars) = define_aux evd.defn_evars evd.undf_evars evk body in
+  let (defn_evars, undf_evars) = define_aux ~dorestrict:evk' evd.defn_evars evd.undf_evars evk body in
   { evd with undf_evars = EvMap.add evk' evar_info' undf_evars;
     defn_evars; last_mods; evar_names }, evk'
 
diff --git a/engine/evd.mli b/engine/evd.mli
index abcabe8157..9055dcc86b 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -244,6 +244,9 @@ val restrict : evar -> Filter.t -> ?candidates:constr list ->
 (** Restrict an undefined evar into a new evar by filtering context and
     possibly limiting the instances to a set of candidates *)
 
+val is_restricted_evar : evar_info -> evar option
+(** Tell if an evar comes from restriction of another evar, and if yes, which *)
+
 val downcast : evar -> types -> evar_map -> evar_map
 (** Change the type of an undefined evar to a new type assumed to be a
     subtype of its current type; subtyping must be ensured by caller *)