aboutsummaryrefslogtreecommitdiffhomepage
path: root/checker/univ.mli
Commit message (Expand)AuthorAge
* Fixing the checker w.r.t. wrongly used abstract universe contexts.Gravatar Pierre-Marie Pédrot2017-07-19
* Properly handling polymorphic inductive subtyping in the checker.Gravatar Pierre-Marie Pédrot2017-07-11
* Less footguns in universe handling: remove subst_instance_context.Gravatar Pierre-Marie Pédrot2017-07-11
* 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
* Enable the checking of ind subtyping in checkerGravatar Amin Timany2017-06-16
* Correct coqchk checking subtyping relation for inductivesGravatar Amin Timany2017-06-16
* Correct coqchk reductionGravatar Amin Timany2017-06-16
* Update copyright headers.Gravatar Maxime Dénès2016-01-20
* Protect code against changes in Map interface.Gravatar Maxime Dénès2016-01-06
* Univs: fix checker generating undeclared universes.Gravatar Matthieu Sozeau2015-10-02
* Univs: update checkerGravatar Matthieu Sozeau2015-10-02
* Update headers.Gravatar Maxime Dénès2015-01-12
* Fix checker's treatment of template polymorphicGravatar Matthieu Sozeau2015-01-06
* checker: Change in library on disk values, now using context_sets instead ofGravatar Matthieu Sozeau2014-12-17
* Remove unused substitution functions in checker.Gravatar Matthieu Sozeau2014-09-05
* Fix checker treatment of inductives using subst_instances instead of subst_un...Gravatar Matthieu Sozeau2014-09-05
* Removing dead code in checker/univ.ml.Gravatar Pierre-Marie Pédrot2014-06-10
* Removing explanations of universe inconsistencies from the checker. TheyGravatar Pierre-Marie Pédrot2014-06-10
* Providing the checker with its own version of the Univ file.Gravatar Pierre-Marie Pédrot2014-06-10
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-20 16:44:34 +0000