aboutsummaryrefslogtreecommitdiffhomepage
path: root/engine/engine.mllib
Commit message (Expand)AuthorAge
* Split off Universes functions for minimization.Gravatar Gaëtan Gilbert2018-05-17
* Split off Universes functions about substitutions and constraintsGravatar Gaëtan Gilbert2018-05-17
* Split off Universes functions dealing with generating new universes.Gravatar Gaëtan Gilbert2018-05-17
* Split off Universes functions dealing with names.Gravatar Gaëtan Gilbert2018-05-17
* [api] Relocate `intf` modules according to dependency-order.Gravatar Emilio Jesus Gallego Arias2018-04-23
* [api] Miscellaneous consolidation + moves to engine.Gravatar Emilio Jesus Gallego Arias2017-11-21
* Remove the Sigma (monotonous state) API.Gravatar Maxime Dénès2017-06-06
* Namegen primitives now apply on evar constrs.Gravatar Pierre-Marie Pédrot2017-02-14
* Introducing a new EConstr.t type to perform the nf_evar operation on demand.Gravatar Pierre-Marie Pédrot2016-11-08
* Moving Universes to the engine/ folder.Gravatar Pierre-Marie Pédrot2016-10-30
* Reordering Termops w.r.t. Evd and Namegen in engine folder.Gravatar Pierre-Marie Pédrot2016-10-30
* Moving Ftactic and Geninterp to the engine folder.Gravatar Pierre-Marie Pédrot2016-05-04
* Moving Evarutil and Proofview to engine/Gravatar Pierre-Marie Pédrot2016-03-20
* Adding a notion of monotonous evarmap.Gravatar Pierre-Marie Pédrot2015-10-18
* Dedicated file for universe unification context manipulation.Gravatar Pierre-Marie Pédrot2015-10-17
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-05 03:32:06 +0000