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

5 files changed, 93 insertions, 21 deletions

diff --git a/engine/evarutil.ml b/engine/evarutil.ml
index 339c6a248..eabfb7b39 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 14173e774..ee0fae3d4 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 f1b5419de..324f883e8 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 abcabe815..9055dcc86 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 *)
diff --git a/test-suite/bugs/closed/5757.v b/test-suite/bugs/closed/5757.v
new file mode 100644
index 000000000..0d0f2eed4
--- /dev/null
+++ b/test-suite/bugs/closed/5757.v
@@ -0,0 +1,76 @@
+(* Check that resolved status of evars follows "restrict" *)
+
+Axiom H : forall (v : nat), Some 0 = Some v -> True.
+Lemma L : True.
+eapply H with _;
+match goal with
+  | |- Some 0 = Some ?v => change (Some (0+0) = Some v)
+end.
+Abort.
+
+(* The original example *)
+
+Set Default Proof Using "Type".
+
+Module heap_lang.
+
+Inductive expr :=
+  | InjR (e : expr).
+
+Inductive val :=
+  | InjRV (v : val).
+
+Bind Scope val_scope with val.
+
+Fixpoint of_val (v : val) : expr :=
+  match v with
+  | InjRV v => InjR (of_val v)
+  end.
+
+Fixpoint to_val (e : expr) : option val := None.
+
+End heap_lang.
+Export heap_lang.
+
+Module W.
+Inductive expr :=
+  | Val (v : val)
+  (* Sums *)
+  | InjR (e : expr).
+
+Fixpoint to_expr (e : expr) : heap_lang.expr :=
+  match e with
+  | Val v => of_val v
+  | InjR e => heap_lang.InjR (to_expr e)
+  end.
+
+End W.
+
+
+
+Section Tests.
+
+  Context (iProp: Type).
+  Context (WPre: expr -> Prop).
+
+  Context (tac_wp_alloc :
+             forall (e : expr) (v : val),
+               to_val e = Some v -> WPre e).
+
+  Lemma push_atomic_spec (x: val) :
+    WPre (InjR (of_val x)).
+  Proof.
+(* This works. *)
+eapply tac_wp_alloc with _.
+match goal with
+  | |- to_val ?e = Some ?v =>
+    change (to_val (W.to_expr (W.InjR (W.Val x))) = Some v)
+end.
+Undo. Undo.
+(* This is fixed *)
+eapply tac_wp_alloc with _;
+match goal with
+  | |- to_val ?e = Some ?v =>
+    change (to_val (W.to_expr (W.InjR (W.Val x))) = Some v)
+end.
+Abort.