aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/indtypes.ml
Commit message (Expand)AuthorAge
* Indtypes: remove unused is_unit.Gravatar Gaëtan Gilbert2018-07-03
* Swapping Context and Constr: defining declarations on constr in Constr.Gravatar Hugo Herbelin2018-06-27
* Adapt the kernel to generate proper data for mutual records.Gravatar Pierre-Marie Pédrot2018-06-23
* Using more general information for primitive records.Gravatar Pierre-Marie Pédrot2018-06-23
* Change the proj_ind field from MutInd.t to inductive.Gravatar Pierre-Marie Pédrot2018-06-23
* Remove the proj_body field from the kernel.Gravatar Pierre-Marie Pédrot2018-06-17
* Remove the proj_eta field of the kernel.Gravatar Pierre-Marie Pédrot2018-06-17
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-02 03:40:53 +0000