aboutsummaryrefslogtreecommitdiffhomepage
path: root/engine/universes.ml
Commit message (Expand)AuthorAge
* [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
* | Less footguns in universe handling: remove subst_instance_context.Gravatar Pierre-Marie Pédrot2017-07-11
* | Getting rid of simple calls to AUContext.instance.Gravatar Pierre-Marie Pédrot2017-07-11
* | 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
* Using UInfoInd for universes in inductive typesGravatar Amin Timany2017-06-16
* New datastructure for universes of inductive typesGravatar Amin Timany2017-06-16
* Drop '.' from CErrors.anomaly, insert it in argsGravatar Jason Gross2017-06-02
* Remove unused [open] statementsGravatar Gaetan Gilbert2017-04-27
* Add [_] prefix to unused values which maybe should be keptGravatar Gaetan Gilbert2017-04-27
* Merge branch 'trunk' into pr379Gravatar Maxime Dénès2017-03-24
|\
| * [pp] Remove uses of expensive string_of_ppcmds.Gravatar Emilio Jesus Gallego Arias2017-03-21
* | 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
* Code factorization in 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-12-18 10:42:53 +0000