| Age | Commit message (Collapse) | Author |
|---|
|
Ltac variables were not yet supported.
|
|
|
|
Using it feels nicer this way, with GADT details hidden inside comtactic
|
|
The current implementation of par: is still in the STM, but is optional.
If the STM does not take over it, it defaults to the implementation of
in comTactic which is based on all: (i.e. sequential).
This commit also moved the interpretation of a tactic from g_ltac to
vernac/comTactic which is more appropriate.
Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
|
|
|
|
Add headers to a few files which were missing them.
|
|
|
|
|
|
We remove a few aliases present in the lower layers
[`Genintern/Tactypes`] from `Tacexpr`.
IMHO this enlarges the API for no good purpose, and difficults
analysis.
|
|
This is a function that keeps beeing asked or reimplemented. It doesn't hurt
adding it to the Ltac API.
|
|
We move the last 3 types to more adequate places.
|
|
- move_location to proofs/logic.
- intro_pattern_naming to Namegen.
|
|
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.
|
|
|
|
We follow the suggestions in #402 and turn uses of `Loc.located` in
`vernac` into `CAst.t`. The impact should be low as this change mostly
affects top-level vernaculars.
With this change, we are even closer to automatically map a text
document to its AST in a programmatic way.
|
|
To this extent we factor out the relevant bits to a new file,
ltac_pretype.
|
|
The old algorithm was relying on list membership, which is O(n). This was
nefarious for terms with many binders. We use instead sets in O(log n).
|
|
|
|
|
|
|
|
|
|
ssreflect and coq code
|
|
The new function is interp_glob_closure which is basically a renaming
and generalization of interp_uconstr.
Note a change of semantics that I could however not observe in
practice.
Formerly, interp_uconstr discarded ltac variables bound to names for
interning, but interp_constr did not. Now, both discard them.
We also export the new interp_glob_closure.
|
|
This simplifies the API as before, inference of instances of type
classes was iff a type constraint was given.
We then export these both versions of interp_open_constr.
|
|
|
|
|
|
Now it is a private field, locations are optional.
|
|
|
|
|
|
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.
|
