| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
We implement a new type of "preterms" that represent untyped ASTs, corresponding
to glob_expr in the ML implementations. Ltac2 quotations inside notations are
provided with such preterms, and have to pretype them in order to do anything
of relevance with them.
|
|
Most of these files were introduced after #6543 but used older headers
copied from somewhere else.
|
|
Since Ltac2 cannot be put under the stdlib logical root (some file names
would clash), we move it to the `user-contrib` directory, to avoid adding
another hardcoded path in `coqinit.ml`, following a suggestion by @ejgallego.
Thanks to @Zimmi48 for the thorough documentation review and the
numerous suggestions.
|
