| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
|
|
| |
Due to code reworking, a fastpath got anihilated because the slow path
was computed altogether. We now only compute the slow check whenever the
quick one fails.
|
| | |
|
| | |
|
| |\ |
|
| | |
| |
| |
| |
| | |
This is now useless as this returns evar-constrs, so that all functions acting
on them should be insensitive to evar-normalization.
|
| | |
| |
| |
| |
| |
| | |
This removes quite a few unsafe casts. Unluckily, I had to reintroduce
the old non-module based names for these data structures, because I could
not reproduce easily the same hierarchy in EConstr.
|
| | | |
|
| | | |
|
| | | |
|
| | | |
|
| | | |
|
| | |\
| | |
| | |
| | | |
Was PR#350: tclDISPATCH: more informative error message
|
| |/| | |
|
| | |/
|/|
| |
| |
| |
| |
| |
| |
| | |
"expected _n_ tactics" -> "exected _n_ tactics, was given _k_".
Also affect other similar tacticals from `Proofview`.
I used that for debugging once, I thought I might as well propose it for
mergeing.
|
| | | |
|
| |\ \ |
|
| | |/
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
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.
|
| | |
| |
| |
| | |
Suggested by @ppedrot
|
| |/
|
|
|
|
|
| |
As noted by @ppedrot, the first is redundant. The patch is basically a renaming.
We didn't make the component optional yet, but this could happen in a
future patch.
|
| | |
|
| |
|
|
|
|
| |
module)
For the moment, there is an Error module in compilers-lib/ocamlbytecomp.cm(x)a
|
| |
|
|
|
|
|
|
|
|
| |
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.
|
| | |
|
| | |
|
| | |
|
| |
|
|
|
| |
You can now write [[1, 3-5]:tac.] to apply [tac] on the subgoals
numbered 1 and 3 to 5.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
This patch splits pretty printing representation from IO operations.
- `Pp` is kept in charge of the abstract pretty printing representation.
- The `Feedback` module provides interface for doing printing IO.
The patch continues work initiated for 8.5 and has the following effects:
- The following functions in `Pp`: `pp`, `ppnl`, `pperr`, `pperrnl`,
`pperr_flush`, `pp_flush`, `flush_all`, `msg`, `msgnl`, `msgerr`,
`msgerrnl`, `message` are removed. `Feedback.msg_*` functions must be
used instead.
- Feedback provides different backends to handle output, currently,
`stdout`, `emacs` and CoqIDE backends are provided.
- Clients cannot specify flush policy anymore, thus `pp_flush` et al are
gone.
- `Feedback.feedback` takes an `edit_or_state_id` instead of the old
mix.
Lightly tested: Test-suite passes, Proof General and CoqIDE seem to work.
|
| | |
|
| | |
|
| |
|
Pierre-Marie Pédrot
Matej Kosik
Enrico Tassi
Maxime Dénès
Arnaud Spiwack
Matthieu Sozeau
Matthieu Sozeau
Hugo Herbelin
Emilio Jesus Gallego Arias
Pierre Letouzey
Cyprien Mangin