index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
engine
/
univNames.mli
Age
Commit message (
Expand
)
Author
2020-11-25
Separate interning and pretyping of universes
Gaëtan Gilbert
2020-06-25
Generate names for anonymous polymorphic universes
Gaëtan Gilbert
2020-06-25
Make compute_instance_binders internal to UState
Gaëtan Gilbert
2020-03-18
Update headers in the whole code base.
Théo Zimmermann
2019-06-17
Update ml-style headers to new year.
Théo Zimmermann
2018-12-06
Revise API for global universes.
Gaëtan Gilbert
2018-11-16
Print universe names in subtyping error instead of Var(x).
Gaëtan Gilbert
2018-11-09
Use arrays of names instead of lists in abstract universe names.
Pierre-Marie Pédrot
2018-11-09
Remove remnants of polymorphic instance name registration.
Pierre-Marie Pédrot
2018-11-09
Adding universe names to polymorphic entry instances.
Pierre-Marie Pédrot
2018-09-27
Fix #8478: Undeclared universe anomaly with sections
Gaëtan Gilbert
2018-09-21
Store universe binder names as a mere list of names.
Pierre-Marie Pédrot
2018-06-18
Remove reference name type.
Maxime Dénès
2018-06-12
[api] Misctypes removal: miscellaneous aliases.
Emilio Jesus Gallego Arias
2018-05-17
Split off Universes functions dealing with names.
Gaëtan Gilbert
