aboutsummaryrefslogtreecommitdiffhomepage
path: root/engine/universes.ml
Commit message (Expand)AuthorAge
* 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
* Fix nf_evars_universes_opt_subst: recurse on univs, nf undef evarsGravatar Gaëtan Gilbert2018-04-28
* univ minimization: comment [enforce_uppers]Gravatar Gaëtan Gilbert2018-04-13
* univ minimization [enforce_upper]: replace Option.get with matchGravatar Gaëtan Gilbert2018-04-13
* univ minimization: Partially let-lift [enforce_uppers]Gravatar Gaëtan Gilbert2018-04-13
* univ minimization: rename acc' -> enforce_uppersGravatar Gaëtan Gilbert2018-04-13
* univ minimization: use shadowing moreGravatar Gaëtan Gilbert2018-04-13
* univ minimization: let-lift [not_lower]Gravatar Gaëtan Gilbert2018-04-13
* univ minimization: simplify try-with block around find_instsGravatar Gaëtan Gilbert2018-04-13
* univ minimization: s/[failwith ""]/[raise UpperBoundedAlg]/Gravatar Gaëtan Gilbert2018-04-13
* univ minimization: simplify try-with block around [find u left]Gravatar Gaëtan Gilbert2018-04-13
* univ minimization: comment compare_constraint_typeGravatar Gaëtan Gilbert2018-04-13
* niv minimization: remove [remove_lower] abbreviationGravatar Gaëtan Gilbert2018-04-13
* minimize_univ_variables: bool*bool*univ*lowermap replaced by recordGravatar Gaëtan Gilbert2018-04-13
* minimize_univ_variables: remove [and right] abbreviation.Gravatar Gaëtan Gilbert2018-04-13
* universe normalisation: put equivalence class partition in UGraphGravatar Gaëtan Gilbert2018-04-13
* universe minimization: cleanup using standard combinators, open UnivGravatar Gaëtan Gilbert2018-04-13
* [located] Push inner locations in `reference` to a CAst.t node.Gravatar Emilio Jesus Gallego Arias2018-03-09
* 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
* [lib] Rename Profile to CProfileGravatar Emilio Jesus Gallego Arias2017-12-09
* Merge PR #6290: Rename update to set, Fixes #6196Gravatar Maxime Dénès2017-12-07
|\
| * Rename update to set, fixes #6196Gravatar Paul Steckler2017-12-05
* | Proper nametab handling of global universe namesGravatar Matthieu Sozeau2017-12-01
|/
* Forbid repeated names in universe binders.Gravatar Gaëtan Gilbert2017-11-25
* Universe binders survive sections, modules and compilation.Gravatar Gaëtan Gilbert2017-11-25
* 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] Another large deprecation, `Nameops`Gravatar Emilio Jesus Gallego Arias2017-11-13
* [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
* Merge PR #688: Binding universe constraints in Definition/Inductive/etc...Gravatar Maxime Dénès2017-09-26
|\
| * Allow declaring universe constraints at definition level.Gravatar Matthieu Sozeau2017-09-19
* | Using EConstr equality check in unification.Gravatar Pierre-Marie Pédrot2017-09-08
|/
* Removing template polymorphism for definitions.Gravatar Pierre-Marie Pédrot2017-07-26
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-23 11:53:37 +0000