diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/clenvtac.ml | 20 | ||||
| -rw-r--r-- | proofs/clenvtac.mli | 3 |
2 files changed, 17 insertions, 6 deletions
diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml index ad19bd9b6a..ced684965f 100644 --- a/proofs/clenvtac.ml +++ b/proofs/clenvtac.ml @@ -67,15 +67,17 @@ let clenv_refine with_evars clenv gls = (refine (clenv_cast_meta clenv (clenv_value clenv))) gls +let dft = Unification.default_unify_flags -let res_pf clenv ?(with_evars=false) ?(allow_K=false) gls = - clenv_refine with_evars (clenv_unique_resolver allow_K clenv gls) gls +let res_pf clenv ?(with_evars=false) ?(allow_K=false) ?(flags=dft) gls = + clenv_refine with_evars + (clenv_unique_resolver allow_K ~flags:flags clenv gls) gls -let elim_res_pf_THEN_i clenv tac gls = +let elim_res_pf_THEN_i clenv tac gls = let clenv' = (clenv_unique_resolver true clenv gls) in tclTHENLASTn (clenv_refine false clenv') (tac clenv') gls -let e_res_pf clenv = res_pf clenv ~with_evars:true ~allow_K:false +let e_res_pf clenv = res_pf clenv ~with_evars:true ~allow_K:false ~flags:dft (* [unifyTerms] et [unify] ne semble pas gérer les Meta, en @@ -83,11 +85,19 @@ let e_res_pf clenv = res_pf clenv ~with_evars:true ~allow_K:false d'une même Meta sont compatibles. D'ailleurs le "fst" jette les metas provenant de w_Unify. (Utilisé seulement dans prolog.ml) *) +open Unification + +let fail_quick_unif_flags = { + modulo_conv_on_closed_terms = true; + use_metas_eagerly = false; + modulo_conv = false; +} + (* let unifyTerms m n = walking (fun wc -> fst (w_Unify CONV m n [] wc)) *) let unifyTerms m n gls = let env = pf_env gls in let evd = create_goal_evar_defs (project gls) in - let evd' = Unification.w_unify false env CONV m n evd in + let evd' = w_unify false env CONV ~flags:fail_quick_unif_flags m n evd in tclIDTAC {it = gls.it; sigma = evars_of evd'} let unify m gls = diff --git a/proofs/clenvtac.mli b/proofs/clenvtac.mli index 038f84f017..90d010c801 100644 --- a/proofs/clenvtac.mli +++ b/proofs/clenvtac.mli @@ -17,12 +17,13 @@ open Evd open Clenv open Proof_type open Tacexpr +open Unification (*i*) (* Tactics *) val unify : constr -> tactic val clenv_refine : evars_flag -> clausenv -> tactic -val res_pf : clausenv -> ?with_evars:evars_flag -> ?allow_K:bool -> tactic +val res_pf : clausenv -> ?with_evars:evars_flag -> ?allow_K:bool -> ?flags:unify_flags -> tactic val elim_res_pf_THEN_i : clausenv -> (clausenv -> tactic array) -> tactic (* Compatibility, use res_pf ?with_evars:true instead *) |