aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/declareops.mli
Commit message (Expand)AuthorAge
* Store the conversion oracle in constant and inductive definitions.Gravatar Pierre-Marie Pédrot2018-01-14
* [api] Move structures deprecated in the API to the core.Gravatar Emilio Jesus Gallego Arias2017-11-06
* Separating the module_type and module_body types by using a type parameter.Gravatar Pierre-Marie Pédrot2017-08-29
* Moving the last bits of abtraction-breaking code out of the kernel.Gravatar Pierre-Marie Pédrot2017-07-11
* Safe API for accessing universe constraints of global references.Gravatar Pierre-Marie Pédrot2017-07-11
* Merge PR #853: Clean 'with Definition' implementation.Gravatar Maxime Dénès2017-07-06
|\
* | Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
| * Removing a few suspicious functions from the kernel.Gravatar Pierre-Marie Pédrot2017-07-03
|/
* Clean up universes of constants and inductivesGravatar Amin Timany2017-06-16
* Adding a default safe set of kernel typing flags to Declareops.Gravatar Pierre-Marie Pédrot2016-06-16
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
|\
| * Update copyright headers.Gravatar Maxime Dénès2016-01-20
* | Hashconsing modules.Gravatar Pierre-Marie Pédrot2015-11-15
|/
* Avoid type checking private_constants (side_eff) again during Qed (#4357).Gravatar Enrico Tassi2015-10-28
* Removing dead code.Gravatar Pierre-Marie Pédrot2015-02-02
* Make native compiler handle universe polymorphic definitions.Gravatar Maxime Dénès2015-01-17
* Update headers.Gravatar Maxime Dénès2015-01-12
* selective join/export of the safe_environmentGravatar Enrico Tassi2014-10-13
* library/opaqueTables: enable their use in interactive modeGravatar Enrico Tassi2014-10-13
* 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-22 18:29:05 +0000