Remove reference name type.

reference was defined as Ident or Qualid, but the qualid type already
permits empty paths. So we had effectively two representations for
unqualified names, that were not seen as equal by eq_reference.

We remove the reference type and replace its uses by qualid.

1 files changed, 11 insertions, 10 deletions

diff --git a/engine/univNames.ml b/engine/univNames.ml
index 6ffb4bcf0d..a688401741 100644
--- a/engine/univNames.ml
+++ b/engine/univNames.ml
@@ -14,18 +14,19 @@ open Globnames
 open Nametab
 
 
-let reference_of_level l = CAst.make @@
+let qualid_of_level l =
   match Level.name l with
   | Some (d, n as na)  ->
-     let qid =
-       try Nametab.shortest_qualid_of_universe na
-       with Not_found ->
-         let name = Id.of_string_soft (string_of_int n) in
-         Libnames.make_qualid d name
-     in Libnames.Qualid qid
-  | None -> Libnames.Ident Id.(of_string_soft (Level.to_string l))
-
-let pr_with_global_universes l = Libnames.pr_reference (reference_of_level l)
+    begin
+    try Nametab.shortest_qualid_of_universe na
+    with Not_found ->
+      let name = Id.of_string_soft (string_of_int n) in
+      Libnames.make_qualid d name
+    end
+  | None ->
+    Libnames.qualid_of_ident @@ Id.of_string_soft (Level.to_string l)
+
+let pr_with_global_universes l = Libnames.pr_qualid (qualid_of_level l)
 
 (** Global universe information outside the kernel, to handle
     polymorphic universe names in sections that have to be discharged. *)