From ccb173a440fa2eb7105a692c979253edbfe475ee Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Wed, 19 Oct 2016 13:33:28 +0200 Subject: Unification constraint handling (#4763, #5149) Refine fix for bug #4763, fixing #5149 Tactic [Refine.solve_constraints] and global option Adds a new multi-goal tactic [Refine.solve_constraints] that forces solving of unification constraints and evar candidates to be solved. run_tactic now calls [solve_constraints] at every [.], preserving (mostly) the 8.4/8.5 behavior of tactics. The option allows to unset the forced solving unification constraints at each ".", letting the user control the places where the use of heuristics is done. Fix test-suite files too. --- engine/proofview.mli | 1 - 1 file changed, 1 deletion(-) (limited to 'engine/proofview.mli') diff --git a/engine/proofview.mli b/engine/proofview.mli index 725445251..90be2f90a 100644 --- a/engine/proofview.mli +++ b/engine/proofview.mli @@ -373,7 +373,6 @@ val mark_as_unsafe : unit tactic with given up goals cannot be closed. *) val give_up : unit tactic - (** {7 Control primitives} *) (** [tclPROGRESS t] checks the state of the proof after [t]. It it is -- cgit v1.2.3