index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
engine
/
engine.mllib
Commit message (
Expand
)
Author
Age
*
[api] Miscellaneous consolidation + moves to engine.
Emilio Jesus Gallego Arias
2017-11-21
*
Remove the Sigma (monotonous state) API.
Maxime Dénès
2017-06-06
*
Namegen primitives now apply on evar constrs.
Pierre-Marie Pédrot
2017-02-14
*
Introducing a new EConstr.t type to perform the nf_evar operation on demand.
Pierre-Marie Pédrot
2016-11-08
*
Moving Universes to the engine/ folder.
Pierre-Marie Pédrot
2016-10-30
*
Reordering Termops w.r.t. Evd and Namegen in engine folder.
Pierre-Marie Pédrot
2016-10-30
*
Moving Ftactic and Geninterp to the engine folder.
Pierre-Marie Pédrot
2016-05-04
*
Moving Evarutil and Proofview to engine/
Pierre-Marie Pédrot
2016-03-20
*
Adding a notion of monotonous evarmap.
Pierre-Marie Pédrot
2015-10-18
*
Dedicated file for universe unification context manipulation.
Pierre-Marie Pédrot
2015-10-17
*
Moving Proofview_monad to the engine/ folder.
Pierre-Marie Pédrot
2015-02-28
*
Adding a new folder corresponding to the low-level part of the pretyper
Pierre-Marie Pédrot
2015-02-27