aboutsummaryrefslogtreecommitdiff
path: root/kernel/univ.mli
AgeCommit message (Expand)Author
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-09[api] Remove yet another type alias.Emilio Jesus Gallego Arias
2017-12-01Proper nametab handling of global universe namesMatthieu Sozeau
2017-11-24When declaring constants/inductives use ContextSet if monomorphic.Gaëtan Gilbert
2017-11-06[api] Move structures deprecated in the API to the core.Emilio Jesus Gallego Arias
2017-09-19Don't lose names in UState.universe_context.Gaëtan Gilbert
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-11Moving the last bits of abtraction-breaking code out of the kernel.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-11Asserting that monomorphic section variables have no abstracted 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-16New datastructure for universes of inductive typesAmin Timany
2016-01-21Merge branch 'v8.5'Pierre-Marie Pédrot
2016-01-20Update copyright headers.Maxime Dénès
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-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-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
2015-01-12Update headers.Maxime Dénès
2014-10-02Implement module subtyping for polymorphic constants (errors onMatthieu Sozeau
2014-08-30Simplify even further the declaration of primitive projections,Matthieu Sozeau
2014-08-09Adding a primitive to merge ContextSets which is more efficient when onePierre-Marie Pédrot
2014-08-09Cleaning up interface of ContextSet.Pierre-Marie Pédrot
2014-08-03Move to a representation of universe polymorphic constants using indices for ...Matthieu Sozeau
2014-07-31Useless export of Instance.eqeq. We hashcons everything before calling thisPierre-Marie Pédrot
2014-07-21Universe level maps use HMaps.Pierre-Marie Pédrot
2014-07-21Cleanup substitution inside universe instances, only done through subst_fn now,Matthieu Sozeau
2014-07-03Cleanup code related to the constraint solving, which sits now outside theMatthieu Sozeau
2014-07-01Add toplevel commands to declare global universes and constraints.Matthieu Sozeau
2014-06-18Code factorization in LMap.Pierre-Marie Pédrot
2014-06-10Made explanations for universe inconsistencies optional. They are only usedPierre-Marie Pédrot
2014-06-10- Fix substitution of universes which needlessly hashconsed existing universes.Matthieu Sozeau
2014-06-10More cleanup/reorganizing of univ.ml to separate constraint/universe handling...Matthieu Sozeau
2014-06-10Cleanup in Univ, moving code for UniverseConstraints outside the kernel in Un...Matthieu Sozeau
2014-06-10Remove unused function in univMatthieu Sozeau
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-14 05:44:49 +0000