aboutsummaryrefslogtreecommitdiff
path: root/kernel/indtypes.ml
AgeCommit message (Expand)Author
2018-11-09Force the user to provide names when generating abstract universe contexts.Pierre-Marie Pédrot
2018-11-09Adding universe names to polymorphic entry instances.Pierre-Marie Pédrot
2018-10-26Remove a few circumvolutions around parameters of inductive entriesMaxime Dénès
2018-09-24[kernel] Compile with almost all warnings enabled.Emilio Jesus Gallego Arias
2018-09-19Merge PR #8341: Reduce universe redeclarations (catching AlreadyDeclared)Matthieu Sozeau
2018-09-13Avoid repeat univ declaration in cumulative subtyping checkGaëtan Gilbert
2018-09-13Kernel: fully obey mind_entry_templateGaëtan Gilbert
2018-07-24Projections use index representationGaëtan Gilbert
2018-07-03Indtypes: remove unused is_unit.Gaëtan Gilbert
2018-06-27Swapping Context and Constr: defining declarations on constr in Constr.Hugo Herbelin
2018-06-23Adapt the kernel to generate proper data for mutual records.Pierre-Marie Pédrot
2018-06-23Using more general information for primitive records.Pierre-Marie Pédrot
2018-06-23Change the proj_ind field from MutInd.t to inductive.Pierre-Marie Pédrot
2018-06-17Remove the proj_body field from the kernel.Pierre-Marie Pédrot
2018-06-17Remove the proj_eta field of the kernel.Pierre-Marie Pédrot
2018-02-27Update headers following #6543.Théo Zimmermann
2018-02-11Universe instance printer: add optional variance argument.Gaëtan Gilbert
2018-02-10Simplification: cumulativity information is variance information.Gaëtan Gilbert
2018-02-10Fix typo in Univ.CumulativityInfoGaëtan Gilbert
2017-12-30Returning instance instead of substitution in universe context abstraction.Pierre-Marie Pédrot
2017-12-23[api] Also deprecate constructors of Decl_kinds.Emilio Jesus Gallego Arias
2017-11-24When declaring constants/inductives use ContextSet if monomorphic.Gaëtan Gilbert
2017-11-22[api] Deprecate Term destructors, move to ConstrEmilio Jesus Gallego Arias
2017-11-06[api] Move structures deprecated in the API to the core.Emilio Jesus Gallego Arias
2017-11-06[api] Deprecate all legacy uses of Names in core.Emilio Jesus Gallego Arias
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 15:54:13 +0000