aboutsummaryrefslogtreecommitdiffhomepage
path: root/checker/univ.ml
Commit message (Expand)AuthorAge
* A patch renaming equal into eq in the module dealing withGravatar Hugo Herbelin2016-03-22
* Update copyright headers.Gravatar Maxime Dénès2016-01-20
* Univs: fix checker generating undeclared universes.Gravatar Matthieu Sozeau2015-10-02
* Univs: update checkerGravatar Matthieu Sozeau2015-10-02
* Reverting 16 last commits, committed mistakenly using the wrong push command.Gravatar Hugo Herbelin2015-08-02
* Hconsing continuedGravatar Hugo Herbelin2015-08-02
* Fixing bug #4019, and checker blow-up at once.Gravatar Pierre-Marie Pédrot2015-02-11
* Clarifying the implementation of universe hashconsing.Gravatar Pierre-Marie Pédrot2015-02-11
* Update headers.Gravatar Maxime Dénès2015-01-12
* Fix checker's treatment of template polymorphicGravatar Matthieu Sozeau2015-01-06
* Backporting the change in lists of universes to the checker.Gravatar Pierre-Marie Pédrot2014-12-18
* checker: Change in library on disk values, now using context_sets instead ofGravatar Matthieu Sozeau2014-12-17
* Ensuring the good invariants of hashcons table generation in the API.Gravatar Pierre-Marie Pédrot2014-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-27 03:49:45 +0000