aboutsummaryrefslogtreecommitdiff
path: root/library/universes.ml
AgeCommit message (Expand)Author
2016-10-30Moving Universes to the engine/ folder.Pierre-Marie Pédrot
2016-10-24Merge branch 'v8.6'Pierre-Marie Pédrot
2016-10-20Cleanup code according to comments.Matthieu Sozeau
2016-10-20Fix minimization to be insensitive to redundant arcs.Matthieu Sozeau
2016-08-19Make the user_err header an optional parameter.Emilio Jesus Gallego Arias
2016-08-19Remove errorlabstrm in favor of user_errEmilio Jesus Gallego Arias
2016-07-03errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Pierre Letouzey
2016-06-29universes.ml: Minor code cleanupMatthieu Sozeau
2016-06-13Univs: more robust Universe/Constraint decls #4816Matthieu Sozeau
2016-02-13Merge branch 'v8.5'Pierre-Marie Pédrot
2016-02-03Optimizing the universes_of_constr_function.Pierre-Marie Pédrot
2016-01-21Merge branch 'v8.5'Pierre-Marie Pédrot
2016-01-20Update copyright headers.Maxime Dénès
2015-12-08Merge branch 'v8.5'Pierre-Marie Pédrot
2015-12-03Univs: fix bug #4443.Matthieu Sozeau
2015-11-29Merge branch 'v8.5'Pierre-Marie Pédrot
2015-11-27Univs: entirely disallow instantiation of polymorphic constants withMatthieu Sozeau
2015-11-27Avoid recording spurious Set <= Top.i constraints which are alwaysMatthieu Sozeau
2015-11-26More efficient implementation of equality-up-to-universes in Universes.Pierre-Marie Pédrot
2015-11-26More invariants in UState.Pierre-Marie Pédrot
2015-10-29Merge branch 'v8.5'Pierre-Marie Pédrot
2015-10-28Univs: local names handling.Matthieu Sozeau
2015-10-27Fix bugs 4389, 4390 and 4391 due to wrong handling of universe namesMatthieu Sozeau
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: refined handling of assumptionsMatthieu Sozeau
2015-10-02Univs: fix minimization to allow lowering a universe to Set, not Prop.Matthieu Sozeau
2015-10-02Univs: minimization, adapt to graph invariants.Matthieu 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-07-07Univs/minimization: Fix unused variable bug.Matthieu Sozeau
2015-06-26Fix bug #4254 with the help of J.H. JourdanMatthieu Sozeau
2015-06-11Fix bug #3446.Matthieu Sozeau
2015-05-27Fix bug #4159Matthieu Sozeau
2015-04-22Tactical `progress` compares term up to potentially equalisable universes.Arnaud Spiwack
2015-04-09Strengthen minimization: it shouldn't set a universe u to a max if itMatthieu Sozeau
2015-02-24Refactoring in [Constr].Arnaud Spiwack
2015-01-17Univs: proper printing of global and local universe names (onlyMatthieu Sozeau
2015-01-12Update headers.Maxime Dénès
2014-11-23Pass around information on the use of template polymorphism forMatthieu Sozeau
2014-11-10Universes.nf_evars_and_universes_opt_subst substitutes evars eagerly.Pierre-Marie Pédrot
2014-10-13library/opaqueTables: enable their use in interactive modeEnrico Tassi
2014-09-27Add a boolean to indicate the unfolding state of a primitive projection,Matthieu Sozeau
2014-09-24Make eq_pattern_test/eq_test work up to the equivalence of primitiveMatthieu Sozeau
2014-08-25Fix computation of dangling constraints at the end of a proof (bug #3531).Matthieu Sozeau
2014-08-25instanciation is French, instantiation is EnglishJason Gross
2014-08-05Small code simplification.Pierre-Marie Pédrot
2014-08-03Move to a representation of universe polymorphic constants using indices for ...Matthieu Sozeau
2014-07-21More straightforward definition of Universes.add_list_map.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-23 15:05:50 +0000