aboutsummaryrefslogtreecommitdiff
path: root/engine/uState.ml
AgeCommit message (Expand)Author
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
2018-05-08Don't use ref universe_opt_substGaëtan Gilbert
2018-03-09[located] Push inner locations in `reference` to a CAst.t node.Emilio Jesus Gallego Arias
2018-03-09Delayed weak constraints for cumulative inductive types.Gaëtan Gilbert
2018-03-09Statically enforce that ULub is only between levels.Gaëtan Gilbert
2018-03-06Rename some universe minimizing "normalize" functions to "minimize"Gaëtan Gilbert
2018-03-06Deprecate UState aliases in Evd.Gaëtan Gilbert
2018-02-27Update headers following #6543.Théo Zimmermann
2018-02-22[ast] Improve precision of Ast location recognition in serialization.Emilio Jesus Gallego Arias
2018-01-17Merge PR #6298: Fix #6297: handle constraints like (u+1 <= Set/Prop)Maxime Dénès
2017-12-30Moving some universe substitution code out of the kernel.Pierre-Marie Pédrot
2017-12-14Merge PR #6038: [build] Remove coqmktop in favor of ocamlfind.Maxime Dénès
2017-12-11Merge PR #6324: Fix #6323: stronger restrict universe context vs abstract.Maxime Dénès
2017-12-09[lib] Rename Profile to CProfileEmilio Jesus Gallego Arias
2017-12-07Merge PR #6290: Rename update to set, Fixes #6196Maxime Dénès
2017-12-06Fix #6323: stronger restrict universe context vs abstract.Gaëtan Gilbert
2017-12-05Rename update to set, fixes #6196Paul Steckler
2017-12-01Fix #6297: handle constraints like (u+1 <= Set/Prop)Gaëtan Gilbert
2017-12-01Proper nametab handling of global universe namesMatthieu Sozeau
2017-11-25Forbid repeated names in universe binders.Gaëtan Gilbert
2017-11-24Use Entries.constant_universes_entry more.Gaëtan Gilbert
2017-11-24restrict_universe_context: do not prune named universes.Gaëtan Gilbert
2017-11-24Separate checking univ_decls and obtaining universe binder names.Gaëtan Gilbert
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 21:49:30 +0000