aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/indtypes.ml
Commit message (Expand)AuthorAge
* 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
* | 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
* A patch for printing "match" when constructors are defined with let-inGravatar Hugo Herbelin2014-10-20
* Revert d0cd27e209be08ee51a2d609157367f053438a10: giving a different nameGravatar Matthieu Sozeau2014-10-11
* Add a boolean to indicate the unfolding state of a primitive projection,Gravatar Matthieu Sozeau2014-09-27
* Fix generation of inductive elimination principle for primitive records.Gravatar Matthieu Sozeau2014-09-10
* Fix primitive projections declarations for inductive records.Gravatar Matthieu Sozeau2014-09-05
* Simplify even further the declaration of primitive projections,Gravatar Matthieu Sozeau2014-08-30
* Add test-suite file. Compute the name for the record binder in theGravatar Matthieu Sozeau2014-08-29
* Change the way primitive projections are declared to the kernel.Gravatar Matthieu Sozeau2014-08-28
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-28 02:10:20 +0000