aboutsummaryrefslogtreecommitdiffhomepage
path: root/checker/univ.mli
Commit message (Expand)AuthorAge
* Infrastructure for ocamldebug on the checkerGravatar Gaëtan Gilbert2018-05-13
* Replace invalid tag @raises in ocamldoc comments with @raiseGravatar mrmr19932018-03-05
* Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
* Adding a sanity check on inductive variance subtyping.Gravatar Pierre-Marie Pédrot2018-02-15
* Simplification: cumulativity information is variance information.Gravatar Gaëtan Gilbert2018-02-10
* Moving some universe substitution code out of the kernel.Gravatar Pierre-Marie Pédrot2017-12-30
* Do not hashcons universes beforehand.Gravatar Pierre-Marie Pédrot2017-09-01
* deprecate Pp.std_ppcmds type aliasGravatar Matej Košík2017-07-27
* 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-22 10:47:18 +0000