aboutsummaryrefslogtreecommitdiff
path: root/kernel/univ.ml
AgeCommit message (Expand)Author
2017-10-16Use type nonrec in some functor arguments.Gaëtan Gilbert
2017-09-01Do not hashcons universes beforehand.Pierre-Marie Pédrot
2017-07-27deprecate Pp.std_ppcmds type aliasMatej Košík
2017-07-13The only abstraction-breaking function in Univ is now AUContext.instance.Pierre-Marie Pédrot
2017-07-11Cleaning up the implementation of module subtyping in the kernel.Pierre-Marie Pédrot
2017-07-11Less footguns in universe handling: remove subst_instance_context.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-16Simplify Univ.mlAmin Timany
2017-06-16Squashed commit of the following:Amin Timany
2017-06-16Check subtyping of inductive types in KernelAmin Timany
2017-06-16Using UInfoInd for universes in inductive typesAmin Timany
2017-06-16New datastructure for universes of inductive typesAmin Timany
2017-06-02Drop '.' from CErrors.anomaly, insert it in argsJason Gross
2017-04-27Remove some unused values and typesGaetan Gilbert
2016-12-02Document changesMatthieu Sozeau
2016-11-30Slightly more efficient [Univ.super] implemMatthieu Sozeau
2016-07-03errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Pierre Letouzey
2016-03-30Merge branch 'v8.5'Pierre-Marie Pédrot
2016-03-22A patch renaming equal into eq in the module dealing withHugo Herbelin
2016-01-21Merge branch 'v8.5'Pierre-Marie Pédrot
2016-01-20Update copyright headers.Maxime Dénès
2016-01-17Universes algorithm : clarified commentsJacques-Henri Jourdan
2015-11-29Merge branch 'v8.5'Pierre-Marie Pédrot
2015-11-27Univs: entirely disallow instantiation of polymorphic constants withMatthieu Sozeau
2015-11-23Fix output of universe arcs. (Fix bug #4422)Guillaume Melquiond
2015-11-05Merge branch 'v8.5'Pierre-Marie Pédrot
2015-11-04Univs: update refman, better printers for universe contexts.Matthieu Sozeau
2015-10-29Merge branch 'v8.5'Pierre-Marie Pédrot
2015-10-28Adds support for the virtual machine to perform reduction of universe polymor...Gregory Malecha
2015-10-09Merge branch 'v8.5'Pierre-Marie Pédrot
2015-10-08Univs: fix bug #3807Matthieu Sozeau
2015-10-06Splitting kernel universe code in two modules.Pierre-Marie Pédrot
2015-10-05Univs: fix bug #4288, Print Sorted generated backward < constraints.Matthieu Sozeau
2015-10-02Univs: fix bug #4251, handling of template polymorphic constants.Matthieu Sozeau
2015-10-02Univs (kernel) adapt to new invariantsMatthieu Sozeau
2015-10-02Forcing i > Set for global universes (incomplete)Matthieu Sozeau
2015-10-02Universes: enforce Set <= i for all Type occurrences.Matthieu Sozeau
2015-08-02Reverting 16 last commits, committed mistakenly using the wrong push command.Hugo Herbelin
2015-08-02A patch renaming equal into eq in the module dealing withHugo Herbelin
2015-07-16Modules: fix bug #4294Matthieu Sozeau
2015-07-01Further simplification of the graph traversal in Univ.Pierre-Marie Pédrot
2015-06-24Less closures makes the GC happy.Pierre-Marie Pédrot
2015-06-23Less closures makes the GC happy.Pierre-Marie Pédrot
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-28Fixing bug #3931.Pierre-Marie Pédrot
2015-01-17Univs: proper printing of global and local universe names (onlyMatthieu Sozeau
2015-01-17Make native compiler handle universe polymorphic definitions.Maxime Dénès
2015-01-15Correct restriction of vm_compute when handling universe polymorphicMatthieu Sozeau
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 18:49:31 +0000