aboutsummaryrefslogtreecommitdiffhomepage
path: root/checker/univ.mli
Commit message (Expand)AuthorAge
* 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-06 02:04:50 +0000