aboutsummaryrefslogtreecommitdiff
path: root/engine/uState.mli
AgeCommit message (Expand)Author
2019-11-21[coq] Untabify the whole ML codebase.Emilio Jesus Gallego Arias
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-08-26Make kernel parametric on the lowest universe and fix #9294Matthieu Sozeau
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-06-11Remove the side-effect role from the kernel.Pierre-Marie Pédrot
2019-05-10[api] Remove 8.10 deprecations.Emilio Jesus Gallego Arias
2019-02-17Separate variance and universe fields in inductives.Gaëtan Gilbert
2018-12-06Revise API for global universes.Gaëtan Gilbert
2018-11-12Fix #8908: incorrect refresh of algebraic universes.Gaëtan Gilbert
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-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 about substitutions and constraintsGaëtan Gilbert
2018-05-17Split off Universes functions dealing with names.Gaëtan Gilbert
2018-03-09Delayed weak constraints for cumulative inductive types.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
2017-12-11Merge PR #6368: [api] Remove yet another type alias.Maxime Dénès
2017-12-09[api] Remove yet another type alias.Emilio Jesus Gallego Arias
2017-12-06Fix #6323: stronger restrict universe context vs abstract.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-24Stop exposing UState.universe_context and its Evd wrapper.Gaëtan Gilbert
2017-11-24Separate checking univ_decls and obtaining universe binder names.Gaëtan Gilbert
2017-11-24Use Maps and ids for universe bindersGaëtan Gilbert
2017-11-24Use type Universes.universe_binders.Gaëtan Gilbert
2017-11-22Fix universe polymorphic Program obligations.Matthieu Sozeau
2017-11-06[api] Move structures deprecated in the API to the core.Emilio Jesus Gallego Arias
2017-09-19Document UState.universe_context.Gaëtan Gilbert
2017-09-19Don't lose names in UState.universe_context.Gaëtan Gilbert
2017-09-19proof_global: cleanup and comment close_proofMatthieu Sozeau
2017-09-19Allow declaring universe constraints at definition level.Matthieu Sozeau
2017-07-27deprecate Pp.std_ppcmds type aliasMatej Košík
2017-06-05Univs: fix bug #5365, generation of u+k <= v constraintsMatthieu Sozeau
2016-06-09Adding a bit of documentation in the mli.Pierre-Marie Pédrot
2016-02-19Allowing to attach location to universes in UState.Pierre-Marie Pédrot
2015-12-05Fixing compilation of mli documentation.Hugo Herbelin
2015-12-01Remove unneeded fixpoint in normalize_context_set. Note that it is noMatthieu Sozeau
2015-10-30Merge branch 'v8.5'Pierre-Marie Pédrot
2015-10-29Merge branch 'v8.5'Pierre-Marie Pédrot
2015-10-17Clarifying and documenting the UState API.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 18:39:38 +0000