| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
| |
We do up to `Term` which is the main bulk of the changes.
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
| |
This ensures that the API is self-contained and is, well, an API.
Before this patch, the contents of `API.mli` bore little relation with
what was used by the plugins [example: `Metasyntax` in tacentries.ml].
Many missing types had to be added.
A sanity check of the `API.mli` file can be done with:
`ocamlfind ocamlc -rectypes -package camlp5 -I lib API/API.mli`
|
| | |
|
| |
|
|
|
|
|
| |
Unluckily, this forces replacing a lot of code in plugins, because the API
defined the type of goals and tactics in Proof_type, and by the no-alias rule,
this was the only one. But Proof_type was already implicitly deprecated, so
that the API should have relied on Tacmach instead.
|
| | |
|
| | |
|
| |\ |
|
| | | |
|
| | | |
|
| |/
|
|
|
|
|
|
|
|
|
|
| |
This completes the Loc.ghost removal, the idea is to gear the API
towards optional, but uniform, location handling.
We don't print <unknown> anymore in the case there is no location.
This is what the test suite expects.
The old printing logic for located items was a bit inconsistent as
it sometimes printed <unknown> and other times it printed nothing as
the caller checked for `is_ghost` upstream.
|
| |\ |
|
| | | |
|
| |/
|
|
|
| |
reconsider_conv_pbs -> reconsider_unif_constraints
consider_remaining_unif_problems -> solve_unif_constraints_with_heuristics
|
| |
|
Emilio Jesus Gallego Arias
Matej Košík
Pierre-Marie Pédrot
Gaetan Gilbert
Enrico Tassi
Matthieu Sozeau