| Commit message (Collapse) | Author | Age |
| |
|
| |
|
|
|
|
|
|
|
|
|
| |
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.
|
| |
|
| |
|
| |
|
| |
|
|\ |
|
| | |
|
|/
|
|
| |
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.
|