| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-11-23 | Remove the unsafe camlp5 API from the Coq codebase. | Pierre-Marie Pédrot | |
| 2018-11-17 | [vernacextend] Consolidate extension points API | Emilio Jesus Gallego Arias | |
| We group the extension API and datatypes under `Vernacextend`. This means that the base plugin dependency is now `coq.vernac` from `coq.stm`. This is quite important as for example the LSP server won't like to link the STM in. LTAC still depends on the STM by means of the ltac_profile part tho. The next step could be to move the extension point below `Vernacexpr`. | |||
| 2018-11-13 | [vernac] Rename Vernacinterp to Vernacextend and move extension functions there. | Emilio Jesus Gallego Arias | |
| This PR fixes an issues that was bugging me for some time, namely that `Vernacinterp` really means `Vernacextend`. We thus rename the file and move the associated functions there, which were incorrectly placed in `Vernacentries`. Note the beneficial effects on reducing the `.mli` API. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |