diff options
author | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-08-15 14:27:29 +0200 |
---|---|---|
committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-08-15 14:27:29 +0200 |
commit | 8bc0159095cb0230a50c55a1611c8b77134a6060 (patch) | |
tree | 4fe9861ba7720c4266215785acfcc82fb41b5a5f /proofs | |
parent | aae3c3b42a9bad20ebde4a139e6de660fbb8e042 (diff) |
More self-contained code for tclWITHHOLES.
Diffstat (limited to 'proofs')
-rw-r--r-- | proofs/refiner.ml | 33 | ||||
-rw-r--r-- | proofs/refiner.mli | 4 |
2 files changed, 0 insertions, 37 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 diff --git a/proofs/refiner.mli b/proofs/refiner.mli index 58f9b9617..ea1677f06 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 |