aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/declareops.mli
Commit message (Expand)AuthorAge
* Move to a representation of universe polymorphic constants using indices for ...Gravatar Matthieu Sozeau2014-08-03
* Adapt universe polymorphic branch to new handling of futures for delayed proofs.Gravatar Matthieu Sozeau2014-05-06
* Initial work on reintroducing old-style polymorphism for compatibility (the s...Gravatar Matthieu Sozeau2014-05-06
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06
* New compilation mode -vi2voGravatar Enrico Tassi2014-02-26
* Future: ported to Ephemeron + exception enhancingGravatar gareuselesinge2013-10-18
* Removing a bunch of generic equalities.Gravatar ppedrot2013-09-27
* Declareops + Modops : more clever substitutionsGravatar letouzey2013-08-20
* enhance marshallable option for freeze (minor TODO in safe_typing)Gravatar gareuselesinge2013-08-08
* State Transaction MachineGravatar gareuselesinge2013-08-08
* Revised infrastructure for lazy loading of opaque proofsGravatar letouzey2013-04-02
* kernel/declarations becomes a pure mliGravatar letouzey2013-02-26
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-27 15:16:13 +0000