Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Merge PR #7898: Remove camlp4 remains | 2018-07-11 | |
|\ | |||
| * | Introduce a Pcoq.Entry module for functions that ought to be exported. | 2018-07-07 | |
| | | | | | | | | | | | | | | | | | | | | We deprecate the corresponding functions in Pcoq.Gram. The motivation is that the Gram module is used as an argument to Camlp5 functors, so that it is not stable by extension. Enforcing that its type is literally the one Camlp5 expects ensures robustness to extension statically. Some really internal functions have been bluntly removed. It is unlikely that they are used by external plugins. | ||
* | | fix syntax of .mlg | 2018-07-03 | |
| | | |||
* | | [vernac] use plain strings as attribute names | 2018-07-03 | |
| | | | | | | | | The concrete syntax is still restricted to identifiers. | ||
* | | [vernac] indentation | 2018-07-03 | |
| | | |||
* | | [vernac] Generic syntax for flags/attributes | 2018-07-03 | |
| | | |||
* | | [vernac] Generic parsing rules for attributes | 2018-07-03 | |
| | | |||
* | | [vernac] Concrete syntax for attributes | 2018-07-03 | |
|/ | |||
* | Port g_vernac to the homebrew GEXTEND parser. | 2018-06-29 | |