| Commit message (Expand) | Author | Age | |
|---|---|---|---|
| * | Put all plugins behind an "API". |  Matej Kosik | 2017-06-07 |
| * | Merge PR#696: Trunk+cleanup constr of global |  Maxime Dénès | 2017-06-01 |
| |\ | |||
| * | | Adding "epose", "eset", "eremember" which allow to set terms with |  Hugo Herbelin | 2017-05-30 |
| * | | Adding "eassert", "eenough", "epose proof", which allow to state | Hugo Herbelin | 2017-05-30 |
| | * | Ltac cleanup: no more constr_of_global calls |  Matthieu Sozeau | 2017-05-29 |
| |/ | |||
| * | [location] Make location optional in Loc.located |  Emilio Jesus Gallego Arias | 2017-04-25 |
| * | [location] Remove Loc.ghost. | Emilio Jesus Gallego Arias | 2017-04-25 |
| * | [location] Use located in tactics. | Emilio Jesus Gallego Arias | 2017-04-24 |
| * | [location] Use located in misctypes. | Emilio Jesus Gallego Arias | 2017-04-24 |
| * | Attempt to improve error message when "apply in" fail. | Hugo Herbelin | 2017-03-15 |
| * | Merge PR#395: Allow hintdb to be parameters in a Ltac definition or | Maxime Dénès | 2017-02-27 |
| * | Ltac as a plugin. |  Pierre-Marie Pédrot | 2017-02-17 |
 |
index : coq | |
| the Coq proof assistant |
| aboutsummaryrefslogtreecommitdiffhomepage |