diff options
| -rw-r--r-- | proofs/clenvtac.ml | 19 | ||||
| -rw-r--r-- | proofs/clenvtac.mli | 2 | ||||
| -rw-r--r-- | tactics/class_tactics.ml | 2 | ||||
| -rw-r--r-- | tactics/eauto.ml4 | 2 |
4 files changed, 13 insertions, 12 deletions
diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml index 6873bbb11..941d789dd 100644 --- a/proofs/clenvtac.ml +++ b/proofs/clenvtac.ml @@ -104,14 +104,15 @@ let fail_quick_unif_flags = { } (* let unifyTerms m n = walking (fun wc -> fst (w_Unify CONV m n [] wc)) *) -let unifyTerms ?(flags=fail_quick_unif_flags) m n gls = - let env = pf_env gls in - let evd = create_goal_evar_defs (project gls) in - try +let unify ?(flags=fail_quick_unif_flags) m = + Proofview.Goal.raw_enter begin fun gl -> + let env = Tacmach.New.pf_env gl in + let n = Tacmach.New.pf_nf_concl gl in + let evd = create_goal_evar_defs (Proofview.Goal.sigma gl) in + try let evd' = w_unify env evd CONV ~flags m n in - tclIDTAC {it = gls.it; sigma = evd'; } + Proofview.V82.tclEVARS evd' with e when Errors.noncritical e -> - tclFAIL 0 (Errors.print e) gls - -let unify ?(flags=fail_quick_unif_flags) m gls = - let n = pf_concl gls in unifyTerms ~flags m n gls + (** This is Tacticals.tclFAIL *) + Proofview.tclZERO (FailError (0, lazy (Errors.print e))) + end diff --git a/proofs/clenvtac.mli b/proofs/clenvtac.mli index 173eb32e3..3cfe1f315 100644 --- a/proofs/clenvtac.mli +++ b/proofs/clenvtac.mli @@ -13,7 +13,7 @@ open Tacexpr open Unification (** Tactics *) -val unify : ?flags:unify_flags -> constr -> tactic +val unify : ?flags:unify_flags -> constr -> unit Proofview.tactic val clenv_refine : evars_flag -> ?with_classes:bool -> clausenv -> tactic val res_pf : clausenv -> ?with_evars:evars_flag -> ?flags:unify_flags -> tactic diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index 31fbc0661..f11c027ad 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -98,7 +98,7 @@ let e_give_exact flags poly (c,clenv) gl = else c, gl in let t1 = pf_type_of gl c in - tclTHEN (Clenvtac.unify ~flags t1) (exact_no_check c) gl + tclTHEN (Proofview.V82.of_tactic (Clenvtac.unify ~flags t1)) (exact_no_check c) gl let unify_e_resolve poly flags (c,clenv) gls = let clenv' = if poly then fst (Clenv.refresh_undefined_univs clenv) else clenv in diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4 index bc3ad026c..98e7d3ff5 100644 --- a/tactics/eauto.ml4 +++ b/tactics/eauto.ml4 @@ -34,7 +34,7 @@ let eauto_unif_flags = { auto_unif_flags with Unification.modulo_delta = full_tr let e_give_exact ?(flags=eauto_unif_flags) c gl = let t1 = (pf_type_of gl c) and t2 = pf_concl gl in if occur_existential t1 || occur_existential t2 then - tclTHEN (Clenvtac.unify ~flags t1) (exact_no_check c) gl + tclTHEN (Proofview.V82.of_tactic (Clenvtac.unify ~flags t1)) (exact_no_check c) gl else Proofview.V82.of_tactic (exact_check c) gl let assumption id = e_give_exact (mkVar id) |