diff options
| author | Matthieu Sozeau | 2019-10-08 19:59:35 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2020-03-13 16:16:05 +0100 |
| commit | 89d13a553d340ae2a49853597155ab45c0f5a0f4 (patch) | |
| tree | 5d9764883c5ac11929307802a827422cd7afd742 /tactics/class_tactics.mli | |
| parent | 45e83041ee129a541fdf17a8c50dd6e9e0e81262 (diff) | |
Implementing postponed constraints in TC resolution
A constraint can be stuck if it does not match any of the declared modes
for its head (if there are any). In that case, the subgoal is postponed
and the next ones are tried. We do a fixed point computation until there
are no stuck subgoals or the set does not change (it is impossible to
make it grow, as asserted in the code, because it is always a subset of
the initial goals)
This allows constraints on classes with modes to be treated as if they were
in any order (yay for stability of solutions!). Also, ultimately it should
free us to launch resolutions more agressively (avoiding issues like the
ones seen in PR #10762).
Add more examples of the semantics of TC resolution with apply in test-suite
Properly catch ModeMatchFailure on calls to map_e*
Add fixed bug 9058 to the test-suite
Close #9058
Add documentation
Fixes after Gaëtan's review.
Main change is to not use exceptions for control-flow
Update tactics/class_tactics.ml
Clearer and more efficient mode mismatch dispatch
Co-Authored-By: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
Remove exninfo argument
Diffstat (limited to 'tactics/class_tactics.mli')
| -rw-r--r-- | tactics/class_tactics.mli | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/tactics/class_tactics.mli b/tactics/class_tactics.mli index dc94e6a6fb..02b24bc145 100644 --- a/tactics/class_tactics.mli +++ b/tactics/class_tactics.mli @@ -66,4 +66,6 @@ module Search : sig -> Hints.hint_db list (** The list of hint databases to use *) -> unit Proofview.tactic + (** Note: there might be stuck goals due to mode declarations + remaining even in case of success of the tactic. *) end |