index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
engine
/
universes.mli
Age
Commit message (
Expand
)
Author
2017-12-09
[api] Remove yet another type alias.
Emilio Jesus Gallego Arias
2017-12-01
Proper nametab handling of global universe names
Matthieu Sozeau
2017-11-25
Allow local universe renaming in Print.
Gaëtan Gilbert
2017-11-24
Use Maps and ids for universe binders
Gaëtan Gilbert
2017-11-22
[api] A few more minor deprecation notices.
Emilio Jesus Gallego Arias
2017-11-06
[api] Move structures deprecated in the API to the core.
Emilio Jesus Gallego Arias
2017-11-06
[api] Deprecate all legacy uses of Names in core.
Emilio Jesus Gallego Arias
2017-09-08
Using EConstr equality check in unification.
Pierre-Marie Pédrot
2017-07-27
deprecate Pp.std_ppcmds type alias
Matej Košík
2017-07-17
Merge PR #781: Remove dead code [Universes.simplify_universe_context]
Maxime Dénès
2017-07-13
Safer API for constr_of_global, and getting rid of unsafe_constr_of_global.
Pierre-Marie Pédrot
2017-07-04
Bump year in headers.
Pierre-Marie Pédrot
2017-06-20
Remove dead code [Universes.simplify_universe_context]
Gaëtan Gilbert
2017-06-16
Clean up universes of constants and inductives
Amin Timany
2017-06-16
Squashed commit of the following:
Amin Timany
2017-06-16
Check subtyping of inductive types in Kernel
Amin Timany
2017-06-16
New datastructure for universes of inductive types
Amin Timany
2017-04-11
Update various comments to use "template polymorphism"
Gaetan Gilbert
2017-03-31
Make the Constr.kind_of_term type parametric in sorts and universes.
Pierre-Marie Pédrot
2017-02-14
Evarconv API using EConstr.
Pierre-Marie Pédrot
2016-10-31
Stronger static invariant in equality upto universes.
Pierre-Marie Pédrot
2016-10-30
Moving Universes to the engine/ folder.
Pierre-Marie Pédrot
