In "progress", extending the set of evars w/o solving an existing one is

no longer considered a progress (this prepares generally having tactics
with arguments that contains holes that are added to the goal sigma).
Incidentally, made that "clear" now restricts evars only if the
restriction is really needed.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12602 85f007b7-540e-0410-9357-904b9bb8a0f7

3 files changed, 17 insertions, 13 deletions

diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 0613a35016..dc1784f40c 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -452,11 +452,13 @@ let rec check_and_clear_in_constr evdref err ids c =
 	      with ClearDependencyError (rid,err) ->
 		raise (ClearDependencyError (List.assoc rid rids,err)) in
 
-	    let env = Sign.fold_named_context push_named nhyps ~init:(empty_env) in
-	    let ev'= e_new_evar evdref env ~src:(evar_source evk !evdref) nconcl in
+            if rids = [] then c else begin
+	      let env = Sign.fold_named_context push_named nhyps ~init:(empty_env) in
+	      let ev'= e_new_evar evdref env ~src:(evar_source evk !evdref) nconcl in
 	      evdref := Evd.define evk ev' !evdref;
 	      let (evk',_) = destEvar ev' in
-		mkEvar(evk', Array.of_list nargs)
+	      mkEvar(evk', Array.of_list nargs)
+            end
 
       | _ -> map_constr (check_and_clear_in_constr evdref err ids) c
 
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index 1c47b8b00d..9035bb54db 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -91,6 +91,7 @@ module EvarInfoMap = struct
   let remove evc k = ExistentialMap.remove k evc
   let mem evc k = ExistentialMap.mem k evc
   let fold = ExistentialMap.fold
+  let exists evc f = ExistentialMap.fold (fun k v b -> b || f k v) evc false
 
   let add evd evk newinfo =  ExistentialMap.add evk newinfo evd
 
@@ -312,9 +313,11 @@ module EvarMap = struct
   let existential_value (sigma,_) = EvarInfoMap.existential_value sigma
   let existential_type (sigma,_) = EvarInfoMap.existential_type sigma
   let existential_opt_value (sigma,_) = EvarInfoMap.existential_opt_value sigma
-  let eq_evar_map x y = x == y ||
-    (EvarInfoMap.equal eq_evar_info (fst x) (fst y) &&
-      UniverseMap.equal (=) (snd x) (snd y))
+  let progress_evar_map (sigma1,sm1 as x) (sigma2,sm2 as y) = not (x == y) &&
+    (EvarInfoMap.exists sigma1
+      (fun k v -> v.evar_body = Evar_empty &&
+        (EvarInfoMap.find sigma2 k).evar_body <> Evar_empty)
+    || not (UniverseMap.equal (=) sm1 sm2))
 
   let merge e e' = fold (fun n v sigma -> add sigma n v) e' e
 
@@ -427,10 +430,9 @@ type evar_map =
 
 (*** Lifting primitive from EvarMap. ***)
 
-(* spiwack: this function seems to be used only for the definition of the progress
-    tactical. I would recommand not using it in other places. *)
-let eq_evar_map d1 d2 =
-  EvarMap.eq_evar_map d1.evars d2.evars
+(* HH: The progress tactical now uses this function. *)
+let progress_evar_map d1 d2 =
+  EvarMap.progress_evar_map d1.evars d2.evars
 
 (* spiwack: tentative. It might very well not be the semantics we want
      for merging evar_map *)
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index bffcf1cc64..fed11f1ffa 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -121,9 +121,9 @@ type evar_map
 
 (* Unification state and existential variables *)
 
-(* spiwack: this function seems to be used only for the definition of the progress
-    tactical. I would recommand not using it in other places. *)
-val eq_evar_map : evar_map -> evar_map -> bool
+(* Assuming that the second map extends the first one, this says if
+   some existing evar has been refined *)
+val progress_evar_map : evar_map -> evar_map -> bool
 
 val empty : evar_map
 val is_empty : evar_map -> bool