aboutsummaryrefslogtreecommitdiffhomepage
path: root/engine/uState.mli
Commit message (Expand)AuthorAge
* Remove reference name type.Gravatar Maxime Dénès2018-06-18
* [api] Misctypes removal: miscellaneous aliases.Gravatar Emilio Jesus Gallego Arias2018-06-12
* [api] Move `Constrexpr` to the `interp` module.Gravatar Emilio Jesus Gallego Arias2018-05-31
* [api] Remove deprecated objects in engine / interp / libraryGravatar Emilio Jesus Gallego Arias2018-05-30
* Split off Universes functions about substitutions and constraintsGravatar Gaëtan Gilbert2018-05-17
* Split off Universes functions dealing with names.Gravatar Gaëtan Gilbert2018-05-17
* Delayed weak constraints for cumulative inductive types.Gravatar Gaëtan Gilbert2018-03-09
* Rename some universe minimizing "normalize" functions to "minimize"Gravatar Gaëtan Gilbert2018-03-06
* Deprecate UState aliases in Evd.Gravatar Gaëtan Gilbert2018-03-06
* Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
* [ast] Improve precision of Ast location recognition in serialization.Gravatar Emilio Jesus Gallego Arias2018-02-22
* Merge PR #6368: [api] Remove yet another type alias.Gravatar Maxime Dénès2017-12-11
|\
| * [api] Remove yet another type alias.Gravatar Emilio Jesus Gallego Arias2017-12-09
* | Fix #6323: stronger restrict universe context vs abstract.Gravatar Gaëtan Gilbert2017-12-06
|/
* Proper nametab handling of global universe namesGravatar Matthieu Sozeau2017-12-01
* Forbid repeated names in universe binders.Gravatar Gaëtan Gilbert2017-11-25
* Use Entries.constant_universes_entry more.Gravatar Gaëtan Gilbert2017-11-24
* Stop exposing UState.universe_context and its Evd wrapper.Gravatar Gaëtan Gilbert2017-11-24
* Separate checking univ_decls and obtaining universe binder names.Gravatar Gaëtan Gilbert2017-11-24
* Use Maps and ids for universe bindersGravatar Gaëtan Gilbert2017-11-24
* Use type Universes.universe_binders.Gravatar Gaëtan Gilbert2017-11-24
* Fix universe polymorphic Program obligations.Gravatar Matthieu Sozeau2017-11-22
* [api] Move structures deprecated in the API to the core.Gravatar Emilio Jesus Gallego Arias2017-11-06
* Document UState.universe_context.Gravatar Gaëtan Gilbert2017-09-19
* Don't lose names in UState.universe_context.Gravatar Gaëtan Gilbert2017-09-19
* proof_global: cleanup and comment close_proofGravatar Matthieu Sozeau2017-09-19
* Allow declaring universe constraints at definition level.Gravatar Matthieu Sozeau2017-09-19
* deprecate Pp.std_ppcmds type aliasGravatar Matej Košík2017-07-27
* Univs: fix bug #5365, generation of u+k <= v constraintsGravatar Matthieu Sozeau2017-06-05
* Adding a bit of documentation in the mli.Gravatar Pierre-Marie Pédrot2016-06-09
* Allowing to attach location to universes in UState.Gravatar Pierre-Marie Pédrot2016-02-19
* Fixing compilation of mli documentation.Gravatar Hugo Herbelin2015-12-05
* Remove unneeded fixpoint in normalize_context_set. Note that it is noGravatar Matthieu Sozeau2015-12-01
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-10-30
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-10-29
* Clarifying and documenting the UState API.Gravatar Pierre-Marie Pédrot2015-10-17
* Dedicated file for universe unification context manipulation.Gravatar Pierre-Marie Pédrot2015-10-17
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-04 22:57:06 +0000