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

4 files changed, 40 insertions, 14 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
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index c9c956a1ce..be584790b6 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -462,7 +462,7 @@ let weak_progress gls ptree =
   (not (same_goal (List.hd gls.it) ptree.it))
 
 let progress gls ptree =
-  (not (eq_evar_map ptree.sigma gls.sigma)) ||
+  (progress_evar_map ptree.sigma gls.sigma) ||
   (weak_progress gls ptree)
 
 
@@ -940,3 +940,25 @@ let print_pftreestate {tpf = pf; tpfsigma = sigma; tstack = stack } =
            (List.rev stack) ++ str "] is:")) ++ fnl() ++
   !pp_proof sigma (Global.named_context()) pf ++
   Evd.pr_evar_map sigma
+
+(* Check that holes in arguments have been resolved *)
+
+let check_evars sigma evm gl =
+  let origsigma = gl.sigma in
+  let rest =
+    Evd.fold (fun ev evi acc ->
+      if not (Evd.mem origsigma ev) && not (Evd.is_defined sigma ev)
+      then Evd.add acc ev evi else acc)
+      evm Evd.empty
+  in
+  if rest <> Evd.empty then
+    errorlabstrm "apply" (str"Uninstantiated existential "++
+      str(plural (List.length (Evd.to_list rest)) "variable")++str": " ++
+      fnl () ++ pr_evar_map rest);;
+
+let tclWITHHOLES accept_unresolved_holes tac sigma c gl =
+  if sigma == project gl then tac c gl
+  else
+    let res = tclTHEN (tclEVARS sigma) (tac c) gl in
+    if not accept_unresolved_holes then check_evars (fst res).sigma sigma gl;
+    res