Merge PR #13075: Introducing the foundations for a name-alias-agnostic API

Reviewed-by: SkySkimmer
Ack-by: gares
Ack-by: ejgallego

3 files changed, 7 insertions, 7 deletions

diff --git a/library/coqlib.ml b/library/coqlib.ml
index 04a6e159eb..82d1ecacb5 100644
--- a/library/coqlib.ml
+++ b/library/coqlib.ml
@@ -45,7 +45,7 @@ let has_ref s = CString.Map.mem s !table
 
 let check_ind_ref s ind =
   match CString.Map.find s !table with
-  | GlobRef.IndRef r -> eq_ind r ind
+  | GlobRef.IndRef r -> Ind.CanOrd.equal r ind
   | _ -> false
   | exception Not_found -> false
 
@@ -84,7 +84,7 @@ let gen_reference_in_modules locstr dirs s =
   let dirs = List.map make_dir dirs in
   let qualid = qualid_of_string s in
   let all = Nametab.locate_all qualid in
-  let all = List.sort_uniquize GlobRef.Ordered_env.compare all in
+  let all = List.sort_uniquize GlobRef.UserOrd.compare all in
   let these = List.filter (has_suffix_in_dirs dirs) all in
   match these with
     | [x] -> x
diff --git a/library/globnames.ml b/library/globnames.ml
index bc24fbf096..654349dea0 100644
--- a/library/globnames.ml
+++ b/library/globnames.ml
@@ -98,14 +98,14 @@ module ExtRefOrdered = struct
   let equal x y =
     x == y ||
     match x, y with
-    | TrueGlobal rx, TrueGlobal ry -> GlobRef.Ordered_env.equal rx ry
+    | TrueGlobal rx, TrueGlobal ry -> GlobRef.UserOrd.equal rx ry
     | SynDef knx, SynDef kny -> KerName.equal knx kny
     | (TrueGlobal _ | SynDef _), _ -> false
 
   let compare x y =
     if x == y then 0
     else match x, y with
-      | TrueGlobal rx, TrueGlobal ry -> GlobRef.Ordered_env.compare rx ry
+      | TrueGlobal rx, TrueGlobal ry -> GlobRef.UserOrd.compare rx ry
       | SynDef knx, SynDef kny -> KerName.compare knx kny
       | TrueGlobal _, SynDef _ -> -1
       | SynDef _, TrueGlobal _ -> 1
@@ -113,7 +113,7 @@ module ExtRefOrdered = struct
   open Hashset.Combine
 
   let hash = function
-  | TrueGlobal gr -> combinesmall 1 (GlobRef.Ordered_env.hash gr)
+  | TrueGlobal gr -> combinesmall 1 (GlobRef.UserOrd.hash gr)
   | SynDef kn -> combinesmall 2 (KerName.hash kn)
 
 end
diff --git a/library/lib.ml b/library/lib.ml
index 830777003b..fa0a95d366 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -525,8 +525,8 @@ let init () =
 let mp_of_global = let open GlobRef in function
   | VarRef id -> !lib_state.path_prefix.Nametab.obj_mp
   | ConstRef cst -> Names.Constant.modpath cst
-  | IndRef ind -> Names.ind_modpath ind
-  | ConstructRef constr -> Names.constr_modpath constr
+  | IndRef ind -> Names.Ind.modpath ind
+  | ConstructRef constr -> Names.Construct.modpath constr
 
 let rec dp_of_mp = function
   |Names.MPfile dp -> dp