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.

5 files changed, 35 insertions, 36 deletions

diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index df89d9eac..019ec3d27 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -87,7 +87,7 @@ let encode_tuple ({CAst.loc} as r) =
 
 module PrintingInductiveMake =
   functor (Test : sig
-     val encode : reference -> inductive
+     val encode : qualid -> inductive
      val member_message : Pp.t -> bool -> Pp.t
      val field : string
      val title : string
diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli
index 5310455fe..8695d52b1 100644
--- a/pretyping/detyping.mli
+++ b/pretyping/detyping.mli
@@ -87,7 +87,7 @@ val subst_genarg_hook :
 
 module PrintingInductiveMake :
   functor (Test : sig
-    val encode : Libnames.reference -> Names.inductive
+    val encode : Libnames.qualid -> Names.inductive
     val member_message : Pp.t -> bool -> Pp.t
     val field : string
     val title : string
@@ -95,7 +95,7 @@ module PrintingInductiveMake :
     sig
       type t = Names.inductive
       val compare : t -> t -> int
-      val encode : Libnames.reference -> Names.inductive
+      val encode : Libnames.qualid -> Names.inductive
       val subst : substitution -> t -> t
       val printer : t -> Pp.t
       val key : Goptions.option_name
diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml
index 11cfd2040..ba193da60 100644
--- a/pretyping/glob_ops.ml
+++ b/pretyping/glob_ops.ml
@@ -51,7 +51,7 @@ let glob_sort_eq g1 g2 = let open Glob_term in match g1, g2 with
 | GProp, GProp -> true
 | GSet, GSet -> true
 | GType l1, GType l2 ->
-   List.equal (Option.equal (fun (x,m) (y,n) -> Libnames.eq_reference x y && Int.equal m n)) l1 l2
+   List.equal (Option.equal (fun (x,m) (y,n) -> Libnames.qualid_eq x y && Int.equal m n)) l1 l2
 | _ -> false
 
 let binding_kind_eq bk1 bk2 = match bk1, bk2 with
diff --git a/pretyping/glob_term.ml b/pretyping/glob_term.ml
index 54fa5328f..86245d479 100644
--- a/pretyping/glob_term.ml
+++ b/pretyping/glob_term.ml
@@ -33,11 +33,11 @@ type 'a universe_kind =
   | UUnknown
   | UNamed of 'a
 
-type level_info = Libnames.reference universe_kind
+type level_info = Libnames.qualid universe_kind
 type glob_level = level_info glob_sort_gen
 type glob_constraint = glob_level * Univ.constraint_type * glob_level
 
-type sort_info = (Libnames.reference * int) option list
+type sort_info = (Libnames.qualid * int) option list
 type glob_sort = sort_info glob_sort_gen
 
 (** Casts *)
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 9e024b1c2..57c4d363b 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -171,38 +171,37 @@ let _ =
 
 (** Miscellaneous interpretation functions *)
 
-let interp_known_universe_level evd r =
-  let qid = Libnames.qualid_of_reference r in
+let interp_known_universe_level evd qid =
   try
-    match r.CAst.v with
-    | Libnames.Ident id -> Evd.universe_of_name evd id
-    | Libnames.Qualid _ -> raise Not_found
+    let open Libnames in
+    if qualid_is_ident qid then Evd.universe_of_name evd @@ qualid_basename qid
+    else raise Not_found
   with Not_found ->
-    let univ, k = Nametab.locate_universe qid.CAst.v in
+    let univ, k = Nametab.locate_universe qid in
     Univ.Level.make univ k
 
-let interp_universe_level_name ~anon_rigidity evd r =
-  try evd, interp_known_universe_level evd r
+let interp_universe_level_name ~anon_rigidity evd qid =
+  try evd, interp_known_universe_level evd qid
   with Not_found ->
-    match r with (* Qualified generated name *)
-    | {CAst.loc; v=Libnames.Qualid qid} ->
-       let dp, i = Libnames.repr_qualid qid in
-       let num =
-         try int_of_string (Id.to_string i)
-         with Failure _ ->
-           user_err ?loc ~hdr:"interp_universe_level_name"
-                    (Pp.(str "Undeclared global universe: " ++ Libnames.pr_reference r))
-       in
-       let level = Univ.Level.make dp num in
-       let evd =
-         try Evd.add_global_univ evd level
-         with UGraph.AlreadyDeclared -> evd
-       in evd, level
-    | {CAst.loc; v=Libnames.Ident id} -> (* Undeclared *)
-        if not (is_strict_universe_declarations ()) then
-          new_univ_level_variable ?loc ~name:id univ_rigid evd
-        else user_err ?loc ~hdr:"interp_universe_level_name"
-                      (Pp.(str "Undeclared universe: " ++ Id.print id))
+    if Libnames.qualid_is_ident qid then (* Undeclared *)
+      let id = Libnames.qualid_basename qid in
+      if not (is_strict_universe_declarations ()) then
+        new_univ_level_variable ?loc:qid.CAst.loc ~name:id univ_rigid evd
+      else user_err ?loc:qid.CAst.loc ~hdr:"interp_universe_level_name"
+          (Pp.(str "Undeclared universe: " ++ Id.print id))
+    else
+      let dp, i = Libnames.repr_qualid qid in
+      let num =
+        try int_of_string (Id.to_string i)
+        with Failure _ ->
+          user_err ?loc:qid.CAst.loc ~hdr:"interp_universe_level_name"
+            (Pp.(str "Undeclared global universe: " ++ Libnames.pr_qualid qid))
+      in
+      let level = Univ.Level.make dp num in
+      let evd =
+        try Evd.add_global_univ evd level
+        with UGraph.AlreadyDeclared -> evd
+      in evd, level
 
 let interp_universe ?loc evd = function
   | [] -> let evd, l = new_univ_level_variable ?loc univ_rigid evd in
@@ -232,10 +231,10 @@ let interp_known_level_info ?loc evd = function
   | UUnknown | UAnonymous ->
     user_err ?loc ~hdr:"interp_known_level_info"
       (str "Anonymous universes not allowed here.")
-  | UNamed ref ->
-    try interp_known_universe_level evd ref
+  | UNamed qid ->
+    try interp_known_universe_level evd qid
     with Not_found ->
-      user_err ?loc ~hdr:"interp_known_level_info" (str "Undeclared universe " ++ Libnames.pr_reference ref)
+      user_err ?loc ~hdr:"interp_known_level_info" (str "Undeclared universe " ++ Libnames.pr_qualid qid)
 
 let interp_level_info ?loc evd : level_info -> _ = function
   | UUnknown -> new_univ_level_variable ?loc univ_rigid evd