| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2020-03-18 | Update headers in the whole code base. | Théo Zimmermann | |
| Add headers to a few files which were missing them. | |||
| 2019-06-17 | Update ml-style headers to new year. | Théo Zimmermann | |
| 2019-02-06 | Fix #9281: forgotten CeCILL-B headers in ssrmatching plugin. | Théo Zimmermann | |
| 2018-07-07 | Introduce a Pcoq.Entry module for functions that ought to be exported. | Pierre-Marie Pédrot | |
| 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. | |||
| 2018-06-30 | Split the Ssrmatching module between code and grammar rules. | Pierre-Marie Pédrot | |
| Fixes #7857. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |