aboutsummaryrefslogtreecommitdiff
path: root/kernel/univ.mli
AgeCommit message (Expand)Author
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
2014-06-08Function in Univ uselessly exported.Pierre-Marie Pédrot
2014-06-04- Force every universe level to be >= Prop, so one cannot "go under" it anymore.Matthieu Sozeau
2014-06-04- Fix hashing of levels to get the "right" order in universe contexts etc...Matthieu Sozeau
2014-05-06Find a more efficient fix for dealing with template universes:Matthieu Sozeau
2014-05-06- Fix bug preventing apply from unfolding Fixpoints.Matthieu Sozeau
2014-05-06- Fix handling of polymorphic inductive elimination schemes.Matthieu Sozeau
2014-05-06- Rename eq to equal in Univ, document new modules, set interfaces.Matthieu Sozeau
2014-05-06This commit adds full universe polymorphism and fast projections to Coq.Matthieu Sozeau
2014-03-03Fixing Pervasives.equality in extraction.Pierre-Marie Pédrot
2013-10-24Specializing hash functions for widely used types.ppedrot
2013-08-20Universe counters on slaves are in sync with mastergareuselesinge
2013-03-12A version of Univ.check_eq with no anomaly for Evd.set_eq_sortletouzey
2013-02-19Dir_path --> DirPathletouzey
2012-12-14Modulification of dir_pathppedrot
2012-11-26Small cleaning of interface in Univppedrot
2012-10-17univ inconsistency error message gives evidence of a cyclebarras
2012-08-08Updating headers.herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 14:32:03 +0000