aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/indtypes.ml
Commit message (Expand)AuthorAge
* 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
* | | Splitting kernel universe code in two modules.Gravatar Pierre-Marie Pédrot2015-10-06
* | | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-10-02
|\| |
| * | Universes: enforce Set <= i for all Type occurrences.Gravatar Matthieu Sozeau2015-10-02
* | | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-09-06
|\| |
| * | Implementing Herbelin's fix for the "NonPar" bugGravatar mlasson2015-09-03
* | | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-07-18
|\| |
| * | Option -type-in-type: added support in checker and making it contaminatingGravatar Hugo Herbelin2015-07-10
| * | Kernel: primitive projections handling of let-insGravatar Matthieu Sozeau2015-07-09
| * | Template polymorphism: A bug-fix for Bug #4258Gravatar mlasson2015-07-09
| | * Add a corresponding field in `mutual_inductive_entry` (part 2).Gravatar Arnaud Spiwack2015-06-24
| | * Add a corresponding field in `mutual_inductive_entry` (part 1).Gravatar Arnaud Spiwack2015-06-24
| | * Add a field in `mutual_inductive_body` to represent mutual inductive whose po...Gravatar Arnaud Spiwack2015-06-24
| |/ |/|
* | Document the positivity checker.Gravatar Arnaud Spiwack2015-06-23
|/
* Fixing computation of non-recursively uniform arguments in theGravatar Hugo Herbelin2015-03-24
* Fixing wrong rel_context in checking positivity condition.Gravatar Hugo Herbelin2015-03-24
* Univs: When computing the level of an inductive including indices, letsGravatar Matthieu Sozeau2015-02-14
* Removing dead code.Gravatar Pierre-Marie Pédrot2015-02-02
* Fix issue in printing due to de Bruijn bug when constructing compatibilityGravatar Matthieu Sozeau2015-01-13
* Update headers.Gravatar Maxime Dénès2015-01-12
* kernel/ind Change interface of declare_mind and declare_mutualGravatar Matthieu Sozeau2015-01-05
* Fix treatment of universe context in typecheck inductive (was addedGravatar Matthieu Sozeau2014-12-15
* Pass around information on the use of template polymorphism forGravatar Matthieu Sozeau2014-11-23
* Option -type-in-type continued (deactivate test for inferred sort ofGravatar Hugo Herbelin2014-11-19