aboutsummaryrefslogtreecommitdiff
path: root/kernel/univ.ml
AgeCommit message (Expand)Author
2018-06-22Remove hack skipping comparison of algebraic universes in subtyping.Gaëtan Gilbert
2018-06-19Fix Univ.enforce_leq dropped constraints when algebraic on the rightGaë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-04-26Always print explanation for univ inconsistency, rm Flags.univ_printGaëtan Gilbert
2018-04-06Fix #6956: Uncaught exception in bytecode compilationMaxime Dénès
2018-03-09Cumulativity: improve treatment of irrelevant universes.Gaë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-14Merge PR #6713: Fix #6677: Critical bug with VM and universesMaxime Dénès
2018-02-12Fix #6677: Critical bug with VM and universesMaxime Dénès
2018-02-11Universe instance printer: add optional variance argument.Gaëtan Gilbert
2018-02-10Simplification: cumulativity information is variance information.Gaëtan Gilbert
2018-02-10Fix typo in Univ.CumulativityInfoGaëtan Gilbert
2017-12-30Moving some universe substitution code out of the kernel.Pierre-Marie Pédrot
2017-12-30Returning instance instead of substitution in universe context abstraction.Pierre-Marie Pédrot
2017-12-01Proper nametab handling of global universe namesMatthieu Sozeau
2017-11-24When declaring constants/inductives use ContextSet if monomorphic.Gaëtan Gilbert
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-04 00:55:33 +0000