aboutsummaryrefslogtreecommitdiff
path: root/kernel/indtypes.ml
AgeCommit message (Expand)Author
2017-07-11Getting rid of simple calls to AUContext.instance.Pierre-Marie Pédrot
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2017-06-16Clean up universes of constants and inductivesAmin Timany
2017-06-16Fix bugs and add an option for cumulativityAmin Timany
2017-06-16Fix bugsAmin Timany
2017-06-16Add subtyping inference for inductive typesAmin Timany
2017-06-16Correct subtyping check for constructorsAmin Timany
2017-06-16Fix typo in error messageAmin Timany
2017-06-16Check subtyping of inductive types in KernelAmin Timany
2017-06-16Using UInfoInd for universes in inductive typesAmin Timany
2017-06-16Extend definition of inductives to include subtyping infoAmin Timany
2017-06-02Drop '.' from CErrors.anomaly, insert it in argsJason Gross
2017-02-14Introducing contexts parameterized by the inner term type.Pierre-Marie Pédrot
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-18Reuse the typing_flags datatype for inductives.Pierre-Marie Pédrot
2016-06-18Adding a local type-in-type flag in kernel declarations.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-04-14This is an attempt to clarify terminology in choosing variable namesHugo Herbelin
2016-03-18Merge branch 'v8.5'Pierre-Marie Pédrot
2016-03-10Primitive projections: protect kernel from erroneous definitions.Matthieu Sozeau
2016-02-09CLEANUP: Context.{Rel,Named}.Declaration.tMatej Kosik
2016-01-29Merge branch 'v8.5'Pierre-Marie Pédrot
2016-01-26Fixing bde12b70 about reporting ill-formed constructor.Hugo Herbelin
2016-01-21Merge branch 'v8.5'Pierre-Marie Pédrot
2016-01-20Update copyright headers.Maxime Dénès
2016-01-11CLEANUP: kernel/context.ml{,i}Matej Kosik
2015-12-15Fixing e3cefca41b about supposingly simplifying primitive projectionsHugo Herbelin
2015-12-05Slight simplification of the code of primitive projection (in relationHugo Herbelin
2015-11-20Merge branch 'v8.5'Pierre-Marie Pédrot
2015-11-18Fixing fix c71aa6b to primitive projections.Hugo Herbelin
2015-11-18Slightly documenting code for building primitive projections.Hugo Herbelin
2015-11-18Fixing logical bugs in the presence of let-ins in computiong primitiveHugo Herbelin
2015-11-10Merge origin/v8.5 into trunkHugo Herbelin
2015-11-10Dead code from the commit having introduced primitive projections (a4043608).Hugo Herbelin
2015-11-10Fixing a bug in reporting ill-formed constructor.Hugo Herbelin
2015-10-26Merge branch 'v8.5'Pierre-Marie Pédrot
2015-10-22Fixing a bug in reporting ill-formed inductive.Hugo Herbelin
2015-10-15Merge branch 'v8.5'Pierre-Marie Pédrot
2015-10-14Univs: inductives, remove unneeded testMatthieu Sozeau
2015-10-06Splitting kernel universe code in two modules.Pierre-Marie Pédrot
2015-10-02Merge branch 'v8.5'Pierre-Marie Pédrot
2015-10-02Universes: enforce Set <= i for all Type occurrences.Matthieu Sozeau
2015-09-06Merge branch 'v8.5'Pierre-Marie Pédrot
2015-09-03Implementing Herbelin's fix for the "NonPar" bugmlasson
2015-07-18Merge branch 'v8.5'Pierre-Marie Pédrot
2015-07-10Option -type-in-type: added support in checker and making it contaminatingHugo Herbelin
2015-07-09Kernel: primitive projections handling of let-insMatthieu Sozeau
2015-07-09Template polymorphism: A bug-fix for Bug #4258mlasson
2015-06-24Add a corresponding field in `mutual_inductive_entry` (part 2).Arnaud Spiwack
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 14:54:21 +0000