| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2017-11-29 | [lib] [api] Introduce record for `object_prefix` | Emilio Jesus Gallego Arias | |
| This is a minor cleanup adding a record in a try to structure the state living in `Lib`. | |||
| 2017-11-07 | [api] Remove 8.7 ML-deprecated functions. | Emilio Jesus Gallego Arias | |
| 2017-11-03 | Merge PR #6047: A generic printer for ltac values | Maxime Dénès | |
| 2017-11-03 | Merge PR #6027: Mention the migration from Bugzilla to GitHub issues in ↵ | Maxime Dénès | |
| dev/doc/changes. | |||
| 2017-11-02 | Using a specific function to register vernac printers. | Hugo Herbelin | |
| 2017-10-27 | Mention the migration from Bugzilla to GitHub issues in dev/doc/changes. | Théo Zimmermann | |
| 2017-10-26 | Passing around the flag for injection so that tactics calling inj at | Hugo Herbelin | |
| ML level can set the flags themselves. In particular, using injection and discriminate with option "Keep Proofs Equalities" when called from "decide equality" and "Scheme Equality". This fixes bug #5281. | |||
| 2017-10-10 | [configure] Support for flambda flags. | Emilio Jesus Gallego Arias | |
| We add a new option to configure `-flambda-opts` to allow passing custom flags to flambda. Example: ``` ./configure -flambda-opts "-O3 -unbox-closures" ``` | |||
| 2017-10-06 | Extract changes to the XML protocol from its doc | Théo Zimmermann | |
| 2017-08-29 | Move dev/doc/changes to Markdown. | Théo Zimmermann | |
| And remove old French part. And move part about the plugin API to the right section. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |