aboutsummaryrefslogtreecommitdiff
path: root/engine/univNames.ml
AgeCommit message (Expand)Author
2018-10-16Deprecate 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-27Fix #8478: Undeclared universe anomaly with sectionsGaëtan Gilbert
2018-09-21Universe binders are Id, not Name. Never print Var.Gaëtan Gilbert
2018-09-21Best-effort hack to provide a meaningful name for anonymous bound universes.Pierre-Marie Pédrot
2018-09-21Store universe binder names as a mere list of names.Pierre-Marie Pédrot
2018-09-21Removing calls to AUContext.instance.Pierre-Marie Pédrot
2018-09-12Move maps & sets indexed by GlobRef.t into the kernelVincent Laporte
2018-06-18Remove reference name type.Maxime Dénès
2018-06-12[api] Misctypes removal: miscellaneous aliases.Emilio Jesus Gallego Arias
2018-05-17Split off Universes functions dealing with names.Gaëtan Gilbert