More self-contained code for tclWITHHOLES.

3 files changed, 30 insertions, 38 deletions

diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index ba319fdc0e..68fdea652b 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -336,36 +336,3 @@ let tclPUSHEVARUNIVCONTEXT ctx gl =
 
 let tclPUSHCONSTRAINTS cst gl = 
   tclEVARS (Evd.add_constraints (project gl) cst) gl
-
-(* Check that holes in arguments have been resolved *)
-
-let check_evars env sigma extsigma origsigma =
-  let rec is_undefined_up_to_restriction sigma evk =
-    match Evd.evar_body (Evd.find sigma evk) with
-    | Evar_empty -> true
-    | Evar_defined c -> match Term.kind_of_term c with
-      | Term.Evar (evk,l) -> is_undefined_up_to_restriction sigma evk
-      | _ -> 
-        (* We make the assumption that there is no way no refine an
-           evar remaining after typing from the initial term given to
-           apply/elim and co tactics, is it correct? *)
-        false in
-  let rest =
-    Evd.fold_undefined (fun evk evi acc ->
-      if is_undefined_up_to_restriction sigma evk && not (Evd.mem origsigma evk)
-      then
-	evi::acc
-      else
-	acc)
-      extsigma []
-  in
-  match rest with
-  | [] -> ()
-  | evi :: _ ->
-    let (loc,k) = evi.evar_source in
-    let evi = Evarutil.nf_evar_info sigma evi in
-    Pretype_errors.error_unsolvable_implicit loc env sigma evi k None
-
-let gl_check_evars env sigma extsigma gl =
-  let origsigma = gl.sigma in
-  check_evars env sigma extsigma origsigma
diff --git a/proofs/refiner.mli b/proofs/refiner.mli
index 58f9b96172..ea1677f069 100644
--- a/proofs/refiner.mli
+++ b/proofs/refiner.mli
@@ -134,7 +134,3 @@ val tclIFTHENSVELSE   : tactic -> tactic array -> tactic ->tactic
    Equivalent to [(tac1;try tac2)||tac2] *)
 
 val tclIFTHENTRYELSEMUST : tactic -> tactic -> tactic
-
-(* Check that holes in arguments have been resolved *)
-(* spiwack: used in [tclWITHHOLES] both newer and older copy. *)
-val check_evars : Environ.env -> evar_map -> evar_map -> evar_map -> unit
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 22ca1f0441..0c934bde08 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -438,13 +438,42 @@ module New = struct
   let tclPROGRESS t =
     Proofview.tclINDEPENDENT (Proofview.tclPROGRESS t)
 
+  (* Check that holes in arguments have been resolved *)
+
+  let check_evars env sigma extsigma origsigma =
+    let rec is_undefined_up_to_restriction sigma evk =
+      match Evd.evar_body (Evd.find sigma evk) with
+      | Evd.Evar_empty -> true
+      | Evd.Evar_defined c -> match Term.kind_of_term c with
+        | Term.Evar (evk,l) -> is_undefined_up_to_restriction sigma evk
+        | _ -> 
+          (* We make the assumption that there is no way no refine an
+            evar remaining after typing from the initial term given to
+            apply/elim and co tactics, is it correct? *)
+          false in
+    let rest =
+      Evd.fold_undefined (fun evk evi acc ->
+        if is_undefined_up_to_restriction sigma evk && not (Evd.mem origsigma evk)
+        then
+          evi::acc
+        else
+          acc)
+        extsigma []
+    in
+    match rest with
+    | [] -> ()
+    | evi :: _ ->
+      let (loc,k) = evi.Evd.evar_source in
+      let evi = Evarutil.nf_evar_info sigma evi in
+      Pretype_errors.error_unsolvable_implicit loc env sigma evi k None
+
   let tclWITHHOLES accept_unresolved_holes tac sigma x =
     tclEVARMAP >>= fun sigma_initial ->
       if sigma == sigma_initial then tac x
       else
         let check_evars env new_sigma sigma initial_sigma =
           try
-            Refiner.check_evars env new_sigma sigma initial_sigma;
+            check_evars env new_sigma sigma initial_sigma;
             tclUNIT ()
           with e when Errors.noncritical e ->
             tclZERO e