aboutsummaryrefslogtreecommitdiff
path: root/kernel/univ.ml
AgeCommit message (Expand)Author
2020-10-09Merge PR #13143: Drop misleading argument of Pp.h boxcoqbot-app[bot]
2020-10-08Dropping the misleading int argument of Pp.h.Hugo Herbelin
2020-09-28Put type-in-type flag in ugraph.Gaëtan Gilbert
2020-07-06Primitive persistent arraysMaxime Dénès
2020-03-18Update headers in the whole code base.Théo Zimmermann
2020-01-27Small API additions to kernel/univGaëtan Gilbert
2020-01-22Fix #11421 computation of Set+2Gaëtan Gilbert
2020-01-15generate variance data for section universes (not yet used)Gaëtan Gilbert
2019-11-21[coq] Untabify the whole ML codebase.Emilio Jesus Gallego Arias
2019-06-17Update ml-style headers to new year.Théo Zimmermann
2019-05-23Fixing typos - Part 2JPR
2019-05-02Add union in Map interfaceMaxime Dénès
2019-03-14Add a non-cumulative impredicative universe SProp.Gaëtan Gilbert
2019-02-17Separate variance and universe fields in inductives.Gaëtan Gilbert
2018-12-17Make ugraph implementation abstract wrt universe specificsGaëtan Gilbert
2018-12-12checker: check inductive types by roundtrip through the kernel.Gaëtan Gilbert
2018-12-12Merge PR #8974: Fix mod_subst wrt universe polymorphismMaxime Dénès
2018-12-06Revise API for global universes.Gaëtan Gilbert
2018-12-06Fix race condition triggered by fresh universe generationMaxime Dénès
2018-12-05Fix mod_subst wrt universe polymorphismGaëtan Gilbert
2018-11-16We improve a little bit in printing universe constraints signature mismatch.Hugo Herbelin
2018-11-09Use arrays of names instead of lists in abstract universe names.Pierre-Marie Pédrot
2018-11-09Actually store the bound name information in the abstract universe context.Pierre-Marie Pédrot
2018-11-09Force the user to provide names when generating abstract universe contexts.Pierre-Marie Pédrot
2018-11-09Adding universe names to polymorphic entry instances.Pierre-Marie Pédrot
2018-10-16UnivGen.extend_context -> Univ.extend_in_context_setGaëtan Gilbert
2018-10-06[api] Remove (most) 8.9 deprecated objects.Emilio Jesus Gallego Arias
2018-09-27Merge PR #8475: Centralize the reliance on abstract universe context internalsGaëtan Gilbert
2018-09-24[kernel] Compile with almost all warnings enabled.Emilio Jesus Gallego Arias
2018-09-21Remove hash based univ level compareGaëtan Gilbert
2018-09-21Fix printing of abstract universe contexts.Pierre-Marie Pédrot
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 18:34:50 +0000