From 8bc0159095cb0230a50c55a1611c8b77134a6060 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 15 Aug 2014 14:27:29 +0200 Subject: More self-contained code for tclWITHHOLES. --- proofs/refiner.ml | 33 --------------------------------- 1 file changed, 33 deletions(-) (limited to 'proofs/refiner.ml') 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 -- cgit v1.2.3