| 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.
|
|
|
|
| |
And some code simplification.
|
|\ |
|
| |
| |
| |
| |
| | |
To this extent we factor out the relevant bits to a new file,
ltac_pretype.
|
|/ |
|
| |
|
| |
|
| |
|
| |
|
|
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.
|