aboutsummaryrefslogtreecommitdiff
path: root/kernel/inductive.ml
AgeCommit message (Expand)Author
2017-02-14Introducing contexts parameterized by the inner term type.Pierre-Marie Pédrot
2016-07-26Merge remote-tracking branch 'gforge/v8.5' into v8.6Matthieu Sozeau
2016-07-25Fix bug #4876: critical bug in guard condition checker.Matthieu Sozeau
2016-07-03errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Pierre Letouzey
2016-07-01Separate flags for fix/cofix/match reduction and clean reduction function names.Maxime Dénès
2016-06-18Moving the typing_flags to the environment.Pierre-Marie Pédrot
2016-06-16Merge PR #79: Let the kernel assume that a (co-)inductive type is positive.Pierre-Marie Pédrot
2016-06-14Assume totality: dedicated type rather than boolArnaud Spiwack
2016-03-10Removing OCaml deprecated function names from the Lazy module.Pierre-Marie Pédrot
2016-03-05Merge branch 'v8.5'Pierre-Marie Pédrot
2016-03-04This fix is probably not enough to justify that there are no problems withMaxime Dénès
2016-02-15CLEANUP: Simplifying the changes done in "kernel/*"Matej Kosik
2016-02-09CLEANUP: Context.{Rel,Named}.Declaration.tMatej Kosik
2016-01-21Merge branch 'v8.5'Pierre-Marie Pédrot
2016-01-20Update copyright headers.Maxime Dénès
2016-01-11mergeMatej Kosik
2016-01-11CLEANUP: kernel/context.ml{,i}Matej Kosik
2015-12-27Removing dead code.Pierre-Marie Pédrot
2015-12-05Unifying betazeta_applist and prod_applist into a clearer interface.Hugo Herbelin
2015-12-05Moving extended_rel_vect/extended_rel_list to the kernel.Hugo Herbelin
2015-12-05Contracting one extra beta-redex on the fly when typing branches of "match".Hugo Herbelin
2015-12-05A few renaming and simplification in inductive.ml.Hugo Herbelin
2015-10-12Univs: be more restrictive for template polymorphic constants: onlyMatthieu Sozeau
2015-10-02Univs: fix bug #4251, handling of template polymorphic constants.Matthieu Sozeau
2015-07-15Univs/Inductive: fix typechecking of casesMatthieu Sozeau
2015-07-10Unused variables reported by OCaml.Hugo Herbelin
2015-07-09Kernel/Checker: Cleanup fixes of substitutions due to let-ins.Matthieu Sozeau
2015-07-09Template polymorphism: A bug-fix for Bug #4258mlasson
2015-07-07Univs: bug fix.Matthieu Sozeau
2015-06-26Add a flag to deactivate guard checking in the kernel.Arnaud Spiwack
2015-05-12Fix my previous commit on ~polypropPierre Letouzey
2015-05-12Extraction: fix the detection of the "polyprop" situationPierre Letouzey
2015-02-27Add support so that the type of a match in an inductive type with let-inHugo Herbelin
2015-02-02Removing dead code.Pierre-Marie Pédrot
2015-01-17Make native compiler handle universe polymorphic definitions.Maxime Dénès
2015-01-12Update headers.Maxime Dénès
2015-01-06Fix some documentation typos.Guillaume Melquiond
2014-10-11Revert d0cd27e209be08ee51a2d609157367f053438a10: giving a different nameMatthieu Sozeau
2014-09-10Fix generation of inductive elimination principle for primitive records.Matthieu Sozeau
2014-09-04Print [Variant] types with the keyword [Variant].Arnaud Spiwack
2014-08-28Change the way primitive projections are declared to the kernel.Matthieu Sozeau
2014-08-06Relax a bit the guard condition.Maxime Dénès
2014-08-04One more optimization for guard checking of cofixpoints.Maxime Dénès
2014-08-04More optimization in guard checking.Maxime Dénès
2014-08-04Fix an exponential behavior in guard checker for cofixpoints.Maxime Dénès
2014-08-03Move to a representation of universe polymorphic constants using indices for ...Matthieu Sozeau
2014-08-01A tentative uniform naming policy in module Inductiveops.Hugo Herbelin
2014-07-31Optimize check of new subterm relation on match.Maxime Dénès
2014-07-31Fix dynamic computation of recargs for mutual inductives.Maxime Dénès
2014-07-22Minor cleaning.Maxime Dénès
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 17:01:23 +0000