aboutsummaryrefslogtreecommitdiffhomepage
path: root/checker/univ.ml
Commit message (Expand)AuthorAge
* Remove enforce_leq from checkerGravatar Gaëtan Gilbert2018-06-21
* Collecting List.smart_* functions into a module List.Smart.Gravatar Hugo Herbelin2018-05-23
* Collecting Array.smart_* functions into a module Array.Smart.Gravatar Hugo Herbelin2018-05-23
* Infrastructure for ocamldebug on the checkerGravatar Gaëtan Gilbert2018-05-13
* 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
* Drop '.' from CErrors.anomaly, insert it in argsGravatar Jason Gross2017-06-02
* Remove some unused values and typesGravatar Gaetan Gilbert2017-04-27
* errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Gravatar Pierre Letouzey2016-07-03
* 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-05-08 12:50:50 +0000