| Commit message (Collapse) | Author | Age | |
|---|---|---|---|
| * | [printing] Deprecate all printing functions accessing the global proof. |  Emilio Jesus Gallego Arias | 2017-11-21 |
| | | | | | | | | | | | | We'd like to handle proofs functionally we thus recommend not to use printing functions without an explicit context. We also adapt most of the code, making more explicit where the printing environment is coming from. An open task is to refactor some code so we gradually make the `Pfedit.get_current_context ()` disappear. | ||
| * | [API] Remove `open API` in ml files in favor of `-open API` flag. | Emilio Jesus Gallego Arias | 2017-07-17 |
| | | |||
| * | Put "ssreflect" behind "API". |  Matej Košík | 2017-06-07 |
| | | |||
| * | Merge the ssr plugin. |  Maxime Dénès | 2017-06-06 |
 |
index : coq | |
| the Coq proof assistant |
| aboutsummaryrefslogtreecommitdiffhomepage |