Merge PR #7797: Remove reference name type.

5 files changed, 35 insertions, 36 deletions

diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 5a54c6f05..fe49d64c7 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