| 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 |
| | | |||
| * | Removing Proof_type from the API. |  Pierre-Marie Pédrot | 2017-06-16 |
| | | | | | | | | Unluckily, this forces replacing a lot of code in plugins, because the API defined the type of goals and tactics in Proof_type, and by the no-alias rule, this was the only one. But Proof_type was already implicitly deprecated, so that the API should have relied on Tacmach instead. | ||
| * | Dualize the unsafe flag of refine into typecheck and make it mandatory. | Pierre-Marie Pédrot | 2017-06-13 |
| | | |||
| * | Remove (useless) aliases from the API. |  Matej Košík | 2017-06-10 |
| | | |||
| * | 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 |