index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
engine
/
univNames.ml
Age
Commit message (
Expand
)
Author
2020-12-02
Stop calling Id.Map.domain on univ binders every individual universe
Gaëtan Gilbert
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-12
Merge PR #9150: [doc] Enable Warning 50 [incorrect doc comment] and fix comme...
Maxime Dénès
2018-12-09
[doc] Enable Warning 50 [incorrect doc comment] and fix comments.
Emilio Jesus Gallego Arias
2018-12-06
Revise API for global universes.
Gaëtan Gilbert
2018-12-06
Fix race condition triggered by fresh universe generation
Maxime Dénès
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
Actually store the bound name information in the abstract universe context.
Pierre-Marie Pédrot
2018-11-09
Adding universe names to polymorphic entry instances.
Pierre-Marie Pédrot
2018-10-16
Deprecate Global.universes_of_global (replaced by environ version)
Gaëtan Gilbert
2018-10-05
[kernel] Remove section paths from `KerName.t`
Maxime Dénès
2018-09-27
Fix #8478: Undeclared universe anomaly with sections
Gaëtan Gilbert
2018-09-21
Universe binders are Id, not Name. Never print Var.
Gaëtan Gilbert
2018-09-21
Best-effort hack to provide a meaningful name for anonymous bound universes.
Pierre-Marie Pédrot
2018-09-21
Store universe binder names as a mere list of names.
Pierre-Marie Pédrot
2018-09-21
Removing calls to AUContext.instance.
Pierre-Marie Pédrot
2018-09-12
Move maps & sets indexed by GlobRef.t into the kernel
Vincent Laporte
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
