aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/inductive.ml
Commit message (Expand)AuthorAge
* Less footguns in universe handling: remove subst_instance_context.Gravatar Pierre-Marie Pédrot2017-07-11
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
* Clean up universes of constants and inductivesGravatar Amin Timany2017-06-16
* Using UInfoInd for universes in inductive typesGravatar Amin Timany2017-06-16
* Drop '.' from CErrors.anomaly, insert it in argsGravatar Jason Gross2017-06-02
* [cleanup] Unify all calls to the error function.Gravatar Emilio Jesus Gallego Arias2017-05-27
* Introducing contexts parameterized by the inner term type.Gravatar Pierre-Marie Pédrot2017-02-14
* Merge remote-tracking branch 'gforge/v8.5' into v8.6Gravatar Matthieu Sozeau2016-07-26
|\
| * Fix bug #4876: critical bug in guard condition checker.Gravatar Matthieu Sozeau2016-07-25
* | errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Gravatar Pierre Letouzey2016-07-03
* | Separate flags for fix/cofix/match reduction and clean reduction function names.Gravatar Maxime Dénès2016-07-01
* | Moving the typing_flags to the environment.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
* | | Removing OCaml deprecated function names from the Lazy module.Gravatar Pierre-Marie Pédrot2016-03-10
* | | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-03-05
|\ \ \ | | |/ | |/|
| * | This fix is probably not enough to justify that there are no problems withGravatar Maxime Dénès2016-03-04
* | | CLEANUP: Simplifying the changes done in "kernel/*"Gravatar Matej Kosik2016-02-15
* | | CLEANUP: Context.{Rel,Named}.Declaration.tGravatar Matej Kosik2016-02-09
* | | 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
* | | | Removing dead code.Gravatar Pierre-Marie Pédrot2015-12-27
|/ / /
* | | Unifying betazeta_applist and prod_applist into a clearer interface.Gravatar Hugo Herbelin2015-12-05
* | | Moving extended_rel_vect/extended_rel_list to the kernel.Gravatar Hugo Herbelin2015-12-05
* | | Contracting one extra beta-redex on the fly when typing branches of "match".Gravatar Hugo Herbelin2015-12-05
* | | A few renaming and simplification in inductive.ml.Gravatar Hugo Herbelin2015-12-05
|/ /
* | Univs: be more restrictive for template polymorphic constants: onlyGravatar Matthieu Sozeau2015-10-12
* | Univs: fix bug #4251, handling of template polymorphic constants.Gravatar Matthieu Sozeau2015-10-02
* | Univs/Inductive: fix typechecking of casesGravatar Matthieu Sozeau2015-07-15
* | Unused variables reported by OCaml.Gravatar Hugo Herbelin2015-07-10
* | Kernel/Checker: Cleanup fixes of substitutions due to let-ins.Gravatar Matthieu Sozeau2015-07-09
* | Template polymorphism: A bug-fix for Bug #4258Gravatar mlasson2015-07-09
* | Univs: bug fix.Gravatar Matthieu Sozeau2015-07-07
| * Add a flag to deactivate guard checking in the kernel.Gravatar Arnaud Spiwack2015-06-26
|/
* Fix my previous commit on ~polypropGravatar Pierre Letouzey2015-05-12
* Extraction: fix the detection of the "polyprop" situationGravatar Pierre Letouzey2015-05-12
* Add support so that the type of a match in an inductive type with let-inGravatar Hugo Herbelin2015-02-27
* 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
* Fix some documentation typos.Gravatar Guillaume Melquiond2015-01-06
* Revert d0cd27e209be08ee51a2d609157367f053438a10: giving a different nameGravatar Matthieu Sozeau2014-10-11
* Fix generation of inductive elimination principle for primitive records.Gravatar Matthieu Sozeau2014-09-10
* 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
* Relax a bit the guard condition.Gravatar Maxime Dénès2014-08-06
* One more optimization for guard checking of cofixpoints.Gravatar Maxime Dénès2014-08-04
* More optimization in guard checking.Gravatar Maxime Dénès2014-08-04