| Age | Commit message (Expand) | Author |
|---|---|---|
| 2019-06-04 | coqpp: add new ![] specifiers for structured proof interaction | Gaëtan Gilbert |
| 2019-04-09 | [api] [proof] Alert users that `Vernacstate.Proof_global` is not to be used. | Emilio Jesus Gallego Arias |
| 2019-03-27 | [vernac] [stm] Tweak `with_fail` and hopefully fix the semantics. | Emilio Jesus Gallego Arias |
| 2019-03-27 | [vernac] Adapt to removal of imperative proof state. | Emilio Jesus Gallego Arias |
| 2019-01-24 | [STM] explicit handling of parsing states | Enrico Tassi |
| 2018-12-13 | Move shallow state logic to the function preparing state for workers | Maxime Dénès |
| 2018-02-27 | Update headers following #6543. | Théo Zimmermann |
| 2017-11-29 | [proof] [api] Rename proof types in preparation for functionalization. | Emilio Jesus Gallego Arias |
| 2017-11-22 | [plugin] Encapsulate modifiers to vernac commands. | Emilio Jesus Gallego Arias |
| 2017-11-19 | [plugins] Prepare plugin API for functional handling of state. | Emilio Jesus Gallego Arias |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |