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.

8 files changed, 22 insertions, 21 deletions

diff --git a/engine/termops.ml b/engine/termops.ml
index eacc36107..2db2e07bf 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -297,7 +297,7 @@ let has_no_evar sigma =
   with Exit -> false
 
 let pr_evd_level evd = UState.pr_uctx_level (Evd.evar_universe_context evd)
-let reference_of_level evd l = UState.reference_of_level (Evd.evar_universe_context evd) l
+let reference_of_level evd l = UState.qualid_of_level (Evd.evar_universe_context evd) l
 
 let pr_evar_universe_context ctx =
   let open UState in
diff --git a/engine/termops.mli b/engine/termops.mli
index 255494031..f9aa6ba63 100644
--- a/engine/termops.mli
+++ b/engine/termops.mli
@@ -282,7 +282,7 @@ val is_Prop : Evd.evar_map -> constr -> bool
 val is_Set : Evd.evar_map -> constr -> bool
 val is_Type : Evd.evar_map -> constr -> bool
 
-val reference_of_level : Evd.evar_map -> Univ.Level.t -> Libnames.reference
+val reference_of_level : Evd.evar_map -> Univ.Level.t -> Libnames.qualid
 
 (** Combinators on judgments *)
 
diff --git a/engine/uState.ml b/engine/uState.ml
index 0e3ecdbf5..81ab3dd66 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -295,15 +295,15 @@ let constrain_variables diff ctx =
   in
   { ctx with uctx_local = (univs, local); uctx_univ_variables = vars }
   
-let reference_of_level uctx =
+let qualid_of_level uctx =
   let map, map_rev = uctx.uctx_names in 
     fun l ->
-      try CAst.make @@ Libnames.Ident (Option.get (Univ.LMap.find l map_rev).uname)
+      try Libnames.qualid_of_ident (Option.get (Univ.LMap.find l map_rev).uname)
       with Not_found | Option.IsNone ->
-        UnivNames.reference_of_level l
+        UnivNames.qualid_of_level l
 
 let pr_uctx_level uctx l =
-  Libnames.pr_reference (reference_of_level uctx l)
+  Libnames.pr_qualid (qualid_of_level uctx l)
 
 type ('a, 'b) gen_universe_decl = {
   univdecl_instance : 'a; (* Declared universes *)
diff --git a/engine/uState.mli b/engine/uState.mli
index e7e5b39e0..a59e61b89 100644
--- a/engine/uState.mli
+++ b/engine/uState.mli
@@ -171,6 +171,6 @@ val update_sigma_env : t -> Environ.env -> t
 (** {5 Pretty-printing} *)
 
 val pr_uctx_level : t -> Univ.Level.t -> Pp.t
-val reference_of_level : t -> Univ.Level.t -> Libnames.reference
+val qualid_of_level : t -> Univ.Level.t -> Libnames.qualid
 
 val pr_weak : (Univ.Level.t -> Pp.t) -> t -> Pp.t
diff --git a/engine/univNames.ml b/engine/univNames.ml
index 6ffb4bcf0..a68840174 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. *)
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. *)
diff --git a/engine/universes.ml b/engine/universes.ml
index 70601987c..ee9668433 100644
--- a/engine/universes.ml
+++ b/engine/universes.ml
@@ -17,7 +17,7 @@ type universe_binders = UnivNames.universe_binders
 type univ_name_list = UnivNames.univ_name_list
 
 let pr_with_global_universes = UnivNames.pr_with_global_universes
-let reference_of_level = UnivNames.reference_of_level
+let reference_of_level = UnivNames.qualid_of_level
 
 let add_global_universe = UnivNames.add_global_universe
 
diff --git a/engine/universes.mli b/engine/universes.mli
index 46ff33a47..29673de1e 100644
--- a/engine/universes.mli
+++ b/engine/universes.mli
@@ -22,8 +22,8 @@ open Univ
 
 val pr_with_global_universes : Level.t -> Pp.t
 [@@ocaml.deprecated "Use [UnivNames.pr_with_global_universes]"]
-val reference_of_level : Level.t -> Libnames.reference
-[@@ocaml.deprecated "Use [UnivNames.reference_of_level]"]
+val reference_of_level : Level.t -> Libnames.qualid
+[@@ocaml.deprecated "Use [UnivNames.qualid_of_level]"]
 
 val add_global_universe : Level.t -> Decl_kinds.polymorphic -> unit
 [@@ocaml.deprecated "Use [UnivNames.add_global_universe]"]