| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2015-09-27 | Removing subst_defined_metas_evars from Evd. | Pierre-Marie Pédrot | |
| 2015-09-27 | Removing uselessly duplicated function in Evd. | Pierre-Marie Pédrot | |
| 2015-09-26 | Hardening the API of evarmaps. | Pierre-Marie Pédrot | |
| The evar counter has been moved from Evarutil to Evd, and all functions in Evarutil now go through a dedicated primitive to create a fresh evar from an evarmap. | |||
| 2015-09-17 | Merge branch 'v8.5' into trunk | Maxime Dénès | |
| 2015-07-27 | Fix documentation. | Matthieu Sozeau | |
| 2015-07-18 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-07-02 | Merge branch 'v8.5' into trunk | Maxime Dénès | |
| 2015-06-28 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-06-01 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-05-07 | Adding a primitive to the tactic monad to modify the exceptional content. | Pierre-Marie Pédrot | |
| 2015-05-06 | Exposing the minimal amount of internal of the Logic monad in order to | Pierre-Marie Pédrot | |
| allow reusability of the implementation throughout the Coq codebase. We effectively feature a generalized version of the logical monad where the input state, the output state and the inner exception can be arbitrarily chosen. This will allow for more efficient implementations of close variants of the monad. | |||
| 2015-05-05 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-03-23 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-02-28 | Moving Proofview_monad to the engine/ folder. | Pierre-Marie Pédrot | |
| 2015-02-27 | Adding a new folder corresponding to the low-level part of the pretyper | Pierre-Marie Pédrot | |
| together with the tactic monad. The move is not complete yet, because some file candidates for this directory have almost useless dependencies in other ones that should not be moved. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |