| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2016-07-03 | errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib ↵ | Pierre Letouzey | |
| module) For the moment, there is an Error module in compilers-lib/ocamlbytecomp.cm(x)a | |||
| 2016-06-24 | Optimize the clear tactic. | Pierre-Marie Pédrot | |
| We do not allocate a closure in the main loop, and do so only when needed. | |||
| 2016-06-24 | Optimize the clear tactic. | Pierre-Marie Pédrot | |
| We do not check for presence of a variable in a global definition when we know that this variable was not present in the section. | |||
| 2016-06-16 | Document new Hint Mode option. | Matthieu Sozeau | |
| 2016-05-08 | Removing dead code and unused opens. | Pierre-Marie Pédrot | |
| 2016-03-20 | Moving Evarutil and Proofview to engine/ | Pierre-Marie Pédrot | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |