aboutsummaryrefslogtreecommitdiff
path: root/engine/uState.ml
AgeCommit message (Expand)Author
2020-05-25Merge PR #12344: Cleanup noisy prefixesPierre-Marie Pédrot
2020-05-19[universes] [api] Provide UState.from_envEmilio Jesus Gallego Arias
2020-05-18Cleanup: remove noisy "uctx_" prefixes in ustate.mlGaëtan Gilbert
2020-05-13Make explicit that UGraph lower bounds are only of two kinds.Pierre-Marie Pédrot
2020-04-29Merge PR #12158: [univ] API to demote global universesMatthieu Sozeau
2020-04-29[univ] API to demote global universesEnrico Tassi
2020-04-16Make cumulative sprop a typing flag, deprecate command line -sprop-cumulativeGaëtan Gilbert
2020-04-06Clean and fix definitions of options.Théo Zimmermann
2020-03-18Update headers in the whole code base.Théo Zimmermann
2020-02-12Remove Goptions.opt_name fieldGaëtan Gilbert
2019-11-21[coq] Untabify the whole ML codebase.Emilio Jesus Gallego Arias
2019-10-19universes_of_private: return set instead of list of setsGaëtan Gilbert
2019-10-16re-expose UState.demote_seff_univsGaëtan Gilbert
2019-10-09Specialize UState.merge for extend:falseGaëtan Gilbert
2019-10-09Simplify universe handling wrt side effects: rm demote_seff_univsGaëtan Gilbert
2019-10-02simplify branch in process_universe_constraintsGaëtan Gilbert
2019-10-02Postpone the computation of relative constraints in universe unification.Pierre-Marie Pédrot
2019-08-26Make kernel parametric on the lowest universe and fix #9294Matthieu Sozeau
2019-06-25Merge PR #10162: Fix #10161: occur check when defining an algebraic universe.Pierre-Marie Pédrot
2019-06-24Duplicate the type of constant entries in Proof_global.Pierre-Marie Pédrot
2019-06-17Update ml-style headers to new year.Théo Zimmermann
2019-05-14Fix #10161: occur check when defining an algebraic universe.Gaëtan Gilbert
2019-05-10[api] Remove 8.10 deprecations.Emilio Jesus Gallego Arias
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
2019-01-24Global [open Univ] in UStateGaëtan Gilbert
2018-12-12Merge PR #9150: [doc] Enable Warning 50 [incorrect doc comment] and fix comme...Maxime Dénès
2018-12-09[doc] Enable Warning 50 [incorrect doc comment] and fix comments.Emilio Jesus Gallego Arias
2018-12-06Revise API for global universes.Gaëtan Gilbert
2018-12-06Fix race condition triggered by fresh universe generationMaxime Dénès
2018-11-27Fix #8364: making univ algebraic when already equal to another.Gaëtan Gilbert
2018-11-23Local universes for opaque polymorphic constants.Gaëtan Gilbert
2018-11-13Merge PR #8760: Automatically generate names for universes.Pierre-Marie Pédrot
2018-11-12Automatically generate names for universes.Gaëtan Gilbert
2018-11-12Fix #8908: incorrect refresh of algebraic universes.Gaëtan Gilbert
2018-11-09Adding universe names to polymorphic entry instances.Pierre-Marie Pédrot
2018-10-16{Univops->UState}.restrict_universe_contextGaëtan Gilbert
2018-07-25Fix #7900 previous commit fixes a bug when using side effects in obligations.Matthieu Sozeau
2018-07-25kernel: missing check that all universes are declared.Matthieu Sozeau
2018-07-03Remove unused output of Universes.normalize_univ_variablesGaëtan Gilbert
2018-06-18Remove reference name type.Maxime Dénès
2018-06-12[api] Misctypes removal: miscellaneous aliases.Emilio Jesus Gallego Arias
2018-05-31[api] Move `Constrexpr` to the `interp` module.Emilio Jesus Gallego Arias
2018-05-30[api] Remove deprecated objects in engine / interp / libraryEmilio Jesus Gallego Arias
2018-05-17Split off Universes functions for minimization.Gaëtan Gilbert
2018-05-17Make Universes.refresh_constraints internal to UStateGaëtan Gilbert
2018-05-17Split off Universes functions about substitutions and constraintsGaëtan Gilbert
2018-05-17Split off Universes functions dealing with generating new universes.Gaëtan Gilbert
2018-05-17Split off Universes functions dealing with names.Gaëtan Gilbert
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 10:07:03 +0000