aboutsummaryrefslogtreecommitdiff
path: root/engine/univNames.mli
AgeCommit message (Expand)Author
2018-12-06Revise API for global universes.Gaëtan Gilbert
2018-11-16Print universe names in subtyping error instead of Var(x).Gaëtan Gilbert
2018-11-09Use arrays of names instead of lists in abstract universe names.Pierre-Marie Pédrot
2018-11-09Remove remnants of polymorphic instance name registration.Pierre-Marie Pédrot
2018-11-09Adding universe names to polymorphic entry instances.Pierre-Marie Pédrot
2018-09-27Fix #8478: Undeclared universe anomaly with sectionsGaëtan Gilbert
2018-09-21Store universe binder names as a mere list of names.Pierre-Marie Pédrot
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