| Age | Commit message (Collapse) | Author |
|---|
|
Adopting the same format means printing "Ltac foo := ..." and not the
fully qualified name of foo.
|
|
|
|
Add headers to a few files which were missing them.
|
|
|
|
We also slightly change the semantics of the `compat` syntax modifier to
re-express it in terms of the `deprecated` attribute, and we deprecate
it in favor of the latter.
|
|
We remove the `Proof_types` file which was a trivial stub, we also
cleanup a few layers of aliases.
This is not a lot but every little step helps.
|
|
This PR fixes an issues that was bugging me for some time, namely that
`Vernacinterp` really means `Vernacextend`.
We thus rename the file and move the associated functions there, which
were incorrectly placed in `Vernacentries`.
Note the beneficial effects on reducing the `.mli` API.
|
|
|
|
We chose to stick to the most general possible API, even though the macro
will not make full use of the possibilities. It makes explicit the various
data expected to be provided in an orthogonal way.
|
|
This was imposing a bit of useless burden on the API for no good reason.
|
|
We make it possible to deprecate tactics defined by `Ltac`, `Tactic
Notation` or ML.
For the first two variants, we anticipate the syntax of attributes:
`#[deprecated(since = "XX", note = "YY")]`
In ML, the syntax is:
```
let reflexivity_depr =
let open CWarnings in
{ since = "8.5"; note = "Use admit instead." }
TACTIC EXTEND reflexivity DEPRECATED reflexivity_depr
[ "reflexivity" ] -> [ Tactics.intros_reflexivity ]
END
```
A warning is shown at the point where the tactic is used (either
a direct call or when defining another tactic):
Tactic `foo` is deprecated since XX. YY
YY is typically meant to be "Use bar instead.".
|
|
We deprecate the corresponding functions in Pcoq.Gram. The motivation is
that the Gram module is used as an argument to Camlp5 functors, so that
it is not stable by extension. Enforcing that its type is literally the
one Camlp5 expects ensures robustness to extension statically.
Some really internal functions have been bluntly removed. It is unlikely
that they are used by external plugins.
|
|
It was forcing the macro to generate code that was useless.
|
|
reference was defined as Ident or Qualid, but the qualid type already
permits empty paths. So we had effectively two representations for
unqualified names, that were not seen as equal by eq_reference.
We remove the reference type and replace its uses by qualid.
|
|
Today, TACTIC EXTEND generates ad-hoc ML code that registers the tactic
and its parsing rule. Instead, we make it generate a typed AST that is
passed to the parser and a generic tactic execution routine.
PMP has written a small parser that can generate the same typed ASTs
without relying on camlp5, which is overkill for such simple macros.
|
|
|
|
|
|
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`
|
|
|
|
|
|
|
|
|
|
|
|
Now it is a private field, locations are optional.
|
|
The syntax is: TACTIC EXTEND foo AT LEVEL i
This commit makes it possible to define tacticals like the ssreflect
arrow without having to resort to GEXTEND statements and intepretation
hacks.
Note that it simply makes accessible through the ML interface what Tactic
Notation already supports:
Tactic Notation (at level 1) tactic1(t) "=>" ipats(l) := ...
|
|
This commit is essentially moving files around. In particular, the corresponding
plugin still relies on a mllib file rather than a mlpack one. Otherwise, this
causes link-time issues for third-party plugins depending on modules defined
in the Ltac plugin.
|
