diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2016-10-19 13:33:28 +0200 |
|---|---|---|
| committer |  Matthieu Sozeau <mattam@mattam.org> | 2016-10-22 11:32:06 +0200 |
| commit | ccb173a440fa2eb7105a692c979253edbfe475ee (patch) | |
| tree | 4b1dc0c82e3da6b1219adcc195aa6626d5ae3d74 /engine | |
| parent | 379c2403b1cd031091a2271353f26ab24afeb1e5 (diff) | |
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.
Diffstat (limited to 'engine')
| -rw-r--r-- | engine/proofview.ml | 4 | ||||
| -rw-r--r-- | engine/proofview.mli | 1 |
2 files changed, 0 insertions, 5 deletions
diff --git a/engine/proofview.ml b/engine/proofview.ml index 855235d2b..c01879765 100644 --- a/engine/proofview.ml +++ b/engine/proofview.ml @@ -1157,10 +1157,6 @@ let tclLIFT = Proof.lift let tclCHECKINTERRUPT = tclLIFT (NonLogical.make Control.check_for_interrupt) - - - - (*** Compatibility layer with <= 8.2 tactics ***) module V82 = struct type tac = Evar.t Evd.sigma -> Evar.t list Evd.sigma 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 |