aboutsummaryrefslogtreecommitdiffhomepage
path: root/engine
Commit message (Collapse)AuthorAge
...
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-10-06
|
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-10-02
|
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-10-02
|
* Removing meta_with_name from Evd.Gravatar Pierre-Marie Pédrot2015-09-27
|
* Removing subst_defined_metas_evars from Evd.Gravatar Pierre-Marie Pédrot2015-09-27
|
* Removing uselessly duplicated function in Evd.Gravatar Pierre-Marie Pédrot2015-09-27
|
* Hardening the API of evarmaps.Gravatar Pierre-Marie Pédrot2015-09-26
| | | | | | 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.
* Merge branch 'v8.5' into trunkGravatar Maxime Dénès2015-09-17
|
* Fix documentation.Gravatar Matthieu Sozeau2015-07-27
|
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-07-18
|
* Merge branch 'v8.5' into trunkGravatar Maxime Dénès2015-07-02
|
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-06-28
|
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-06-01
|
* Adding a primitive to the tactic monad to modify the exceptional content.Gravatar Pierre-Marie Pédrot2015-05-07
|
* Exposing the minimal amount of internal of the Logic monad in order toGravatar Pierre-Marie Pédrot2015-05-06
| | | | | | | | | 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.
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-05-05
|
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-03-23
|
* Moving Proofview_monad to the engine/ folder.Gravatar Pierre-Marie Pédrot2015-02-28
|
* Adding a new folder corresponding to the low-level part of the pretyperGravatar Pierre-Marie Pédrot2015-02-27
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.