aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/indtypes.ml
Commit message (Expand)AuthorAge
* Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
* Universe instance printer: add optional variance argument.Gravatar Gaëtan Gilbert2018-02-11
* Simplification: cumulativity information is variance information.Gravatar Gaëtan Gilbert2018-02-10
* Fix typo in Univ.CumulativityInfoGravatar Gaëtan Gilbert2018-02-10
* Returning instance instead of substitution in universe context abstraction.Gravatar Pierre-Marie Pédrot2017-12-30
* [api] Also deprecate constructors of Decl_kinds.Gravatar Emilio Jesus Gallego Arias2017-12-23
* When declaring constants/inductives use ContextSet if monomorphic.Gravatar Gaëtan Gilbert2017-11-24
* [api] Deprecate Term destructors, move to ConstrGravatar Emilio Jesus Gallego Arias2017-11-22
* [api] Move structures deprecated in the API to the core.Gravatar Emilio Jesus Gallego Arias2017-11-06
* [api] Deprecate all legacy uses of Names in core.Gravatar Emilio Jesus Gallego Arias2017-11-06
* Getting rid of simple calls to AUContext.instance.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
* Fix bugs and add an option for cumulativityGravatar Amin Timany2017-06-16
* Fix bugsGravatar Amin Timany2017-06-16
* Add subtyping inference for inductive typesGravatar Amin Timany2017-06-16
* Correct subtyping check for constructorsGravatar Amin Timany2017-06-16
* Fix typo in error messageGravatar Amin Timany2017-06-16
* Check subtyping of inductive types in KernelGravatar Amin Timany2017-06-16
* Using UInfoInd for universes in inductive typesGravatar Amin Timany2017-06-16
* Extend definition of inductives to include subtyping infoGravatar Amin Timany2017-06-16
* Drop '.' from CErrors.anomaly, insert it in argsGravatar Jason Gross2017-06-02
* Introducing contexts parameterized by the inner term type.Gravatar Pierre-Marie Pédrot2017-02-14
* 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
* Reuse the typing_flags datatype for inductives.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
|\
* | This is an attempt to clarify terminology in choosing variable namesGravatar Hugo Herbelin2016-04-14
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-03-18
|\ \
| * | Primitive projections: protect kernel from erroneous definitions.Gravatar Matthieu Sozeau2016-03-10
* | | CLEANUP: Context.{Rel,Named}.Declaration.tGravatar Matej Kosik2016-02-09
* | | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-29
|\| |
| * | Fixing bde12b70 about reporting ill-formed constructor.Gravatar Hugo Herbelin2016-01-26
* | | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
|\| |
| * | Update copyright headers.Gravatar Maxime Dénès2016-01-20
* | | CLEANUP: kernel/context.ml{,i}Gravatar Matej Kosik2016-01-11
* | | Fixing e3cefca41b about supposingly simplifying primitive projectionsGravatar Hugo Herbelin2015-12-15
* | | Slight simplification of the code of primitive projection (in relationGravatar Hugo Herbelin2015-12-05
* | | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-11-20
|\| |
| * | Fixing fix c71aa6b to primitive projections.Gravatar Hugo Herbelin2015-11-18
| * | Slightly documenting code for building primitive projections.Gravatar Hugo Herbelin2015-11-18
| * | Fixing logical bugs in the presence of let-ins in computiong primitiveGravatar Hugo Herbelin2015-11-18
* | | Merge origin/v8.5 into trunkGravatar Hugo Herbelin2015-11-10
|\| |
| * | Dead code from the commit having introduced primitive projections (a4043608).Gravatar Hugo Herbelin2015-11-10
| * | Fixing a bug in reporting ill-formed constructor.Gravatar Hugo Herbelin2015-11-10
* | | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-10-26
|\| |
| * | Fixing a bug in reporting ill-formed inductive.Gravatar Hugo Herbelin2015-10-22
* | | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-10-15
|\| |
| * | Univs: inductives, remove unneeded testGravatar Matthieu Sozeau2015-10-14
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-25 12:49:05 +0000