| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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.
|
| | |
|
| | |
|
| |
|
|
| |
goal is under focus and which support returning a relevant output.
|
| |
|
|
|
|
|
|
|
|
| |
unshelve_goals is used to correctly register dependent
subgoals that have to be solved. Resolution may fail to
do so using hints, so we have to put them back as goals
in that case. The shelf is a good interface for doing that.
unifiable can be used outside proofview to detect dependencies
between goals. This might be better in another module.
|
| |
|
|
| |
Fix typo in proofview
|
| |\ |
|
| | | |
|
| | |
| |
| |
| |
| | |
You can now write [[1, 3-5]:tac.] to apply [tac] on the subgoals
numbered 1 and 3 to 5.
|
| |/ |
|
| |
|
Matthieu Sozeau
Pierre-Marie Pédrot
Hugo Herbelin
Matthieu Sozeau
Enrico Tassi
Cyprien Mangin