aboutsummaryrefslogtreecommitdiff
path: root/kernel/univ.ml
AgeCommit message (Expand)Author
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
2015-01-12Update headers.Maxime Dénès
2015-01-07Aligning printing of universe constraints.Hugo Herbelin
2014-12-21Dead code in Univ.Pierre-Marie Pédrot
2014-12-18Cleaning up universe list implementation in Univ.Pierre-Marie Pédrot
2014-12-17Ensuring the good invariants of hashcons table generation in the API.Pierre-Marie Pédrot
2014-12-14Fix merging of name maps in union of universe contexts.Matthieu Sozeau
2014-10-02Implement module subtyping for polymorphic constants (errors onMatthieu Sozeau
2014-09-18Clean a bit of univ.ml, add credits.Matthieu Sozeau
2014-09-05Fix checker treatment of inductives using subst_instances instead of subst_un...Matthieu Sozeau
2014-09-04Fix bug #3559, ensuring a canonical order of universe level quantifications whenMatthieu Sozeau
2014-08-30Simplify even further the declaration of primitive projections,Matthieu Sozeau
2014-08-18Fix pretty-printing of the graph in Print Sorted Universes. Type.0 was larger...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-04Fixing semantics of Univ.Level.equal.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-02 05:15:06 +0000