aboutsummaryrefslogtreecommitdiff
path: root/checker/univ.ml
AgeCommit message (Expand)Author
2018-11-06[checker] Refactor by sharing code with the kernelMaxime Dénès
2018-10-01Fix checker soundness bug with polymorphism capturing global univsGaëtan Gilbert
2018-06-21Remove enforce_leq from checkerGaëtan Gilbert
2018-05-23Collecting List.smart_* functions into a module List.Smart.Hugo Herbelin
2018-05-23Collecting Array.smart_* functions into a module Array.Smart.Hugo Herbelin
2018-05-13Infrastructure for ocamldebug on the checkerGaëtan Gilbert
2018-02-27Update headers following #6543.Théo Zimmermann
2018-02-15Adding a sanity check on inductive variance subtyping.Pierre-Marie Pédrot
2018-02-10Simplification: cumulativity information is variance information.Gaëtan Gilbert
2017-12-30Moving some universe substitution code out of the kernel.Pierre-Marie Pédrot
2017-09-01Do not hashcons universes beforehand.Pierre-Marie Pédrot
2017-07-27deprecate Pp.std_ppcmds type aliasMatej Košík
2017-07-19Fixing the checker w.r.t. wrongly used abstract universe contexts.Pierre-Marie Pédrot
2017-07-11Properly handling polymorphic inductive subtyping in the checker.Pierre-Marie Pédrot
2017-07-11Less footguns in universe handling: remove subst_instance_context.Pierre-Marie Pédrot
2017-07-11Getting rid of simple calls to AUContext.instance.Pierre-Marie Pédrot
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2017-06-16Clean up universes of constants and inductivesAmin Timany
2017-06-16Enable the checking of ind subtyping in checkerAmin Timany
2017-06-16Correct coqchk checking subtyping relation for inductivesAmin Timany
2017-06-16Correct coqchk reductionAmin Timany
2017-06-02Drop '.' from CErrors.anomaly, insert it in argsJason Gross
2017-04-27Remove some unused values and typesGaetan Gilbert
2016-07-03errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Pierre Letouzey
2016-03-22A patch renaming equal into eq in the module dealing withHugo Herbelin
2016-01-20Update copyright headers.Maxime Dénès
2015-10-02Univs: fix checker generating undeclared universes.Matthieu Sozeau
2015-10-02Univs: update checkerMatthieu Sozeau
2015-08-02Reverting 16 last commits, committed mistakenly using the wrong push command.Hugo Herbelin
2015-08-02Hconsing continuedHugo Herbelin
2015-02-11Fixing bug #4019, and checker blow-up at once.Pierre-Marie Pédrot
2015-02-11Clarifying the implementation of universe hashconsing.Pierre-Marie Pédrot
2015-01-12Update headers.Maxime Dénès
2015-01-06Fix checker's treatment of template polymorphicMatthieu Sozeau
2014-12-18Backporting the change in lists of universes to the checker.Pierre-Marie Pédrot
2014-12-17checker: Change in library on disk values, now using context_sets instead ofMatthieu Sozeau
2014-12-17Ensuring the good invariants of hashcons table generation in the API.Pierre-Marie Pédrot
2014-09-05Remove unused substitution functions in checker.Matthieu Sozeau
2014-09-05Fix checker treatment of inductives using subst_instances instead of subst_un...Matthieu Sozeau
2014-06-10Removing dead code in checker/univ.ml.Pierre-Marie Pédrot
2014-06-10Removing explanations of universe inconsistencies from the checker. TheyPierre-Marie Pédrot
2014-06-10Providing the checker with its own version of the Univ file.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-28 04:19:52 +0000