| Commit message (Collapse) | Author | Age |
|---|
| | |
|
| | |
|
| |\ |
|
| | | |
|
| | |
| |
| |
| |
| |
| |
| |
| |
| | |
This allows to factorize code and prevents the unnecessary use of back and
forth conversions between the various types of terms.
Note that functions from typing may now raise errors as PretypeError rather
than TypeError, because they call the proper wrapper. I think that they were
wrongly calling the kernel because of an overlook of open modules.
|
| |/
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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.
|
| | |
|
| |
|
Pierre-Marie Pédrot
Matthieu Sozeau
Hugo Herbelin