aboutsummaryrefslogtreecommitdiffhomepage
path: root/engine/universes.mli
Commit message (Expand)AuthorAge
* Remove unused output of Universes.normalize_univ_variablesGravatar Gaëtan Gilbert2018-07-03
* Remove unused env argument to fresh_sort_in_familyGravatar Gaëtan Gilbert2018-07-03
* Remove reference name type.Gravatar Maxime Dénès2018-06-18
* Split off Universes functions for minimization.Gravatar Gaëtan Gilbert2018-05-17
* Make Universes.refresh_constraints internal to UStateGravatar Gaëtan Gilbert2018-05-17
* Split off Universes functions about substitutions and constraintsGravatar Gaëtan Gilbert2018-05-17
* Move solve_constraint_system near its only use site (comInductive)Gravatar Gaëtan Gilbert2018-05-17
* Split off Universes functions dealing with generating new universes.Gravatar Gaëtan Gilbert2018-05-17
* Split off Universes functions dealing with names.Gravatar Gaëtan Gilbert2018-05-17
* Make set minimization option internal to UniversesGravatar Gaëtan Gilbert2018-05-17
* Don't use ref universe_opt_substGravatar Gaëtan Gilbert2018-05-08
* [api] Rename `global_reference` to `GlobRef.t` to follow kernel style.Gravatar Emilio Jesus Gallego Arias2018-05-04
* universe normalisation: put equivalence class partition in UGraphGravatar Gaëtan Gilbert2018-04-13
* Delayed weak constraints for cumulative inductive types.Gravatar Gaëtan Gilbert2018-03-09
* Statically enforce that ULub is only between levels.Gravatar Gaëtan Gilbert2018-03-09
* Allow using cumulativity without forcing strict constraints.Gravatar Gaëtan Gilbert2018-03-09
* 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
* Simplification: cumulativity information is variance information.Gravatar Gaëtan Gilbert2018-02-10
* Moving some universe substitution code out of the kernel.Gravatar Pierre-Marie Pédrot2017-12-30
* [api] Remove yet another type alias.Gravatar Emilio Jesus Gallego Arias2017-12-09
* Proper nametab handling of global universe namesGravatar Matthieu Sozeau2017-12-01
* Allow local universe renaming in Print.Gravatar Gaëtan Gilbert2017-11-25
* Use Maps and ids for universe bindersGravatar Gaëtan Gilbert2017-11-24
* [api] A few more minor deprecation notices.Gravatar Emilio Jesus Gallego Arias2017-11-22
* [api] Move structures deprecated in the API to the core.Gravatar Emilio Jesus Gallego Arias2017-11-06
* [api] Deprecate all legacy uses of Names in core.Gravatar Emilio Jesus Gallego Arias2017-11-06
* Using EConstr equality check in unification.Gravatar Pierre-Marie Pédrot2017-09-08
* deprecate Pp.std_ppcmds type aliasGravatar Matej Košík2017-07-27
* Merge PR #781: Remove dead code [Universes.simplify_universe_context]Gravatar Maxime Dénès2017-07-17
|\
* | Safer API for constr_of_global, and getting rid of unsafe_constr_of_global.Gravatar Pierre-Marie Pédrot2017-07-13
* | Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
| * Remove dead code [Universes.simplify_universe_context]Gravatar Gaëtan Gilbert2017-06-20
|/
* Clean up universes of constants and inductivesGravatar Amin Timany2017-06-16
* Squashed commit of the following:Gravatar Amin Timany2017-06-16
* Check subtyping of inductive types in KernelGravatar Amin Timany2017-06-16
* New datastructure for universes of inductive typesGravatar Amin Timany2017-06-16
* Update various comments to use "template polymorphism"Gravatar Gaetan Gilbert2017-04-11
* Make the Constr.kind_of_term type parametric in sorts and universes.Gravatar Pierre-Marie Pédrot2017-03-31
* Evarconv API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* Stronger static invariant in equality upto universes.Gravatar Pierre-Marie Pédrot2016-10-31
* Moving Universes to the engine/ folder.Gravatar Pierre-Marie Pédrot2016-10-30
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-05 04:04:00 +0000