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 /proofs/refine.mli | |
| 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 'proofs/refine.mli')
| -rw-r--r-- | proofs/refine.mli | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/proofs/refine.mli b/proofs/refine.mli index 3d140f036..a44632eff 100644 --- a/proofs/refine.mli +++ b/proofs/refine.mli @@ -43,3 +43,8 @@ val with_type : Environ.env -> Evd.evar_map -> val refine_casted : ?unsafe:bool -> Constr.t Sigma.run -> unit tactic (** Like {!refine} except the refined term is coerced to the conclusion of the current goal. *) + +(** {7 Unification constraint handling} *) + +val solve_constraints : unit tactic +(** Solve any remaining unification problems, applying heuristics. *) |