aboutsummaryrefslogtreecommitdiffhomepage
path: root/engine/univNames.mli
diff options
context:
space:
mode:
Diffstat (limited to 'engine/univNames.mli')
-rw-r--r--engine/univNames.mli2
1 files changed, 1 insertions, 1 deletions
diff --git a/engine/univNames.mli b/engine/univNames.mli
index c19aa19d5..837beac26 100644
--- a/engine/univNames.mli
+++ b/engine/univNames.mli
@@ -11,7 +11,7 @@
open Univ
val pr_with_global_universes : Level.t -> Pp.t
-val reference_of_level : Level.t -> Libnames.reference
+val qualid_of_level : Level.t -> Libnames.qualid
(** Global universe information outside the kernel, to handle
polymorphic universes in sections that have to be discharged. *)