| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
|
| |
For now, a few vernacular features were lot in the process, like locating
Ltac definitions. This will be fixed in an upcoming commit.
|
| |
|
|
| |
This commit also fixes range selectors being incorrectly displayed.
|
| |
|
|
|
|
|
| |
This allows to issue a more appropriate message when a notation with a
{ } cannot be defined because of an incompatible level. E.g.:
Notation "{ A } + B" := (sumbool A B) (at level 20).
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
|
|
| |
It seems there were 4 copies of the same function in the code base.
|
| |\ |
|
| | | |
|
| |/
|
|
| |
Now it is a private field, locations are optional.
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Applications of it were not clear/unproven, it made printers more
complex (as they needed to be functors) and as it lacked examples it
confused some people.
The printers now tag unconditionally, it is up to the backends to
interpreted the tags.
Tagging (and indeed the notion of rich document) should be reworked in
a follow-up patch, so they are in sync, but this is a first step.
Tested, test-suite passes.
Notes:
- We remove the `Richprinter` module. It was only used in the
`annotate` IDE protocol call, its output was identical to the normal
printer (or even inconsistent if taggers were not kept manually in
sync).
- Note that Richpp didn't need a single change. In particular, its
main API entry point `Richpp.rich_pp` is not used by anyone.
|
|
|
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.
|
Pierre-Marie Pédrot
Guillaume Melquiond
Hugo Herbelin
Matej Košík
Emilio Jesus Gallego Arias
Maxime Dénès