aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/declarations.mli
Commit message (Expand)AuthorAge
* COMMENT: Declarations.constant_defGravatar Matej Kosik2016-10-26
* CLEANUP: Type alias "Context.section_context" was removedGravatar Matej Kosik2016-08-25
* Reuse the typing_flags datatype for inductives.Gravatar Pierre-Marie Pédrot2016-06-18
* Moving the typing_flags to the environment.Gravatar Pierre-Marie Pédrot2016-06-18
* Adding a local type-in-type flag in kernel declarations.Gravatar Pierre-Marie Pédrot2016-06-18
* Merge PR #79: Let the kernel assume that a (co-)inductive type is positive.Gravatar Pierre-Marie Pédrot2016-06-16
|\
| * Assume totality: dedicated type rather than boolGravatar Arnaud Spiwack2016-06-14
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
|\ \
| * | Update copyright headers.Gravatar Maxime Dénès2016-01-20
* | | mergeGravatar Matej Kosik2016-01-11
|\ \ \ | |/ / |/| |
| * | CLEANUP: kernel/context.ml{,i}Gravatar Matej Kosik2016-01-11
* | | Inclusion of functors with restricted signature is now forbidden (fix #3746)Gravatar Pierre Letouzey2015-12-22
|/ /
* | Avoid type checking private_constants (side_eff) again during Qed (#4357).Gravatar Enrico Tassi2015-10-28
* | Univs: module constraints move to universe contexts as they mightGravatar Matthieu Sozeau2015-10-02
| * Add a field in `constant_body` to track constant whose well-foundedness is as...Gravatar Arnaud Spiwack2015-09-25
* | Option -type-in-type: added support in checker and making it contaminatingGravatar Hugo Herbelin2015-07-10
* | Fixing documentation (see Maxime's mail on coqdev, July 3).Gravatar Hugo Herbelin2015-07-05
| * Add a field in `mutual_inductive_body` to represent mutual inductive whose po...Gravatar Arnaud Spiwack2015-06-24
|/
* Fix vm compiler to refuse to compile code making use of inductives withGravatar Matthieu Sozeau2015-03-25
* Fully fixing bug #3491 (anomaly when building _rect scheme in theGravatar Hugo Herbelin2015-03-25
* Univs: fix bug #3978: carry around the universe context used toGravatar Matthieu Sozeau2015-02-12
* Update headers.Gravatar Maxime Dénès2015-01-12
* Declarations.mli refactoring: module_type_body = module_bodyGravatar Pierre Letouzey2015-01-11
* STM: simplify how the term part of a side effect is retrievedGravatar Enrico Tassi2014-10-13
* Revert d0cd27e209be08ee51a2d609157367f053438a10: giving a different nameGravatar Matthieu Sozeau2014-10-11
* Print [Variant] types with the keyword [Variant].Gravatar Arnaud Spiwack2014-09-04
* Change the way primitive projections are declared to the kernel.Gravatar Matthieu Sozeau2014-08-28
* A tentative uniform naming policy in module Inductiveops.Gravatar Hugo Herbelin2014-08-01
* Reuse universe level substitutions for template polymorphism, fixing performanceGravatar Matthieu Sozeau2014-05-09
* Adapt universe polymorphic branch to new handling of futures for delayed proofs.Gravatar Matthieu Sozeau2014-05-06
* Adapt Y. Bertot's path on private inductives (now the keyword is "Private").Gravatar Yves Bertot2014-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
* Adding a field ci_cstr_nargs to case_info and mind_consnrealargs toGravatar Hugo Herbelin2014-04-28
* Lazyconstr -> OpaqueproofGravatar Enrico Tassi2014-02-26
* New compilation mode -vi2voGravatar Enrico Tassi2014-02-26
* Removing native_name reference from constant_body.Gravatar Maxime Dénès2013-12-28
* ind_tables: properly handling side effectsGravatar gareuselesinge2013-08-30
* Declarations.mli: reorganization of modular structuresGravatar letouzey2013-08-20
* State Transaction MachineGravatar gareuselesinge2013-08-08
* Fixing a bug in the native compiler, introduced by r16363, leading to undefinedGravatar mdenes2013-07-06
* Merging Context and Sign.Gravatar ppedrot2013-04-29
* Splitting Term into five unrelated interfaces:Gravatar ppedrot2013-04-29
* kernel/declarations becomes a pure mliGravatar letouzey2013-02-26
* New implementation of the conversion test, using normalization by evaluation toGravatar mdenes2013-01-22
* Modulification of mod_bound_idGravatar ppedrot2012-12-18
* Modulification of LabelGravatar ppedrot2012-12-18
* Modulification of identifierGravatar ppedrot2012-12-14
* Monomorphization (kernel)Gravatar ppedrot2012-11-22
* Updating headers.Gravatar herbelin2012-08-08
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-25 23:56:05 +0000