aboutsummaryrefslogtreecommitdiff
path: root/kernel/declareops.mli
AgeCommit message (Expand)Author
2014-10-13selective join/export of the safe_environmentEnrico Tassi
2014-10-13library/opaqueTables: enable their use in interactive modeEnrico Tassi
2014-08-03Move to a representation of universe polymorphic constants using indices for ...Matthieu Sozeau
2014-05-06Adapt universe polymorphic branch to new handling of futures for delayed proofs.Matthieu Sozeau
2014-05-06Initial work on reintroducing old-style polymorphism for compatibility (the s...Matthieu Sozeau
2014-05-06This commit adds full universe polymorphism and fast projections to Coq.Matthieu Sozeau
2014-02-26New compilation mode -vi2voEnrico Tassi
2013-10-18Future: ported to Ephemeron + exception enhancinggareuselesinge
2013-09-27Removing a bunch of generic equalities.ppedrot
2013-08-20Declareops + Modops : more clever substitutionsletouzey
2013-08-08enhance marshallable option for freeze (minor TODO in safe_typing)gareuselesinge
2013-08-08State Transaction Machinegareuselesinge
2013-04-02Revised infrastructure for lazy loading of opaque proofsletouzey
2013-02-26kernel/declarations becomes a pure mliletouzey
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 21:40:09 +0000