aboutsummaryrefslogtreecommitdiffhomepage
path: root/engine/universes.mli
Commit message (Expand)AuthorAge
* 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-06-27 06:52:55 +0000