More self-contained code for tclWITHHOLES.

1 files changed, 0 insertions, 33 deletions

diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index ba319fdc0..68fdea652 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