Rename the GlobRef comparison modules following the standard pattern.

12 files changed, 20 insertions, 20 deletions

diff --git a/interp/notation.ml b/interp/notation.ml
index d57c4f3abf..269e20c16e 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -323,7 +323,7 @@ type key =
   | Oth
 
 let key_compare k1 k2 = match k1, k2 with
-| RefKey gr1, RefKey gr2 -> GlobRef.Ordered.compare gr1 gr2
+| RefKey gr1, RefKey gr2 -> GlobRef.CanOrd.compare gr1 gr2
 | RefKey _, Oth -> -1
 | Oth, RefKey _ -> 1
 | Oth, Oth -> 0
diff --git a/interp/reserve.ml b/interp/reserve.ml
index 4418a32645..1d5af3ff39 100644
--- a/interp/reserve.ml
+++ b/interp/reserve.ml
@@ -28,7 +28,7 @@ type key =
 (** TODO: share code from Notation *)
 
 let key_compare k1 k2 = match k1, k2 with
-| RefKey gr1, RefKey gr2 -> GlobRef.Ordered.compare gr1 gr2
+| RefKey gr1, RefKey gr2 -> GlobRef.CanOrd.compare gr1 gr2
 | RefKey _, Oth -> -1
 | Oth, RefKey _ -> 1
 | Oth, Oth -> 0
diff --git a/kernel/names.ml b/kernel/names.ml
index 5f2ecea5f0..f7658df355 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -991,7 +991,7 @@ module GlobRef = struct
 
   (* By default, [global_reference] are ordered on their canonical part *)
 
-  module Ordered = struct
+  module CanOrd = struct
     open Constant.CanOrd
     type t = GlobRefInternal.t
     let compare gr1 gr2 =
@@ -1000,7 +1000,7 @@ module GlobRef = struct
     let hash gr = GlobRefInternal.global_hash_gen hash ind_hash constructor_hash gr
   end
 
-  module Ordered_env = struct
+  module UserOrd = struct
     open Constant.UserOrd
     type t = GlobRefInternal.t
     let compare gr1 gr2 =
@@ -1010,12 +1010,12 @@ module GlobRef = struct
     let hash gr = GlobRefInternal.global_hash_gen hash ind_user_hash constructor_user_hash gr
   end
 
-  module Map = HMap.Make(Ordered)
+  module Map = HMap.Make(CanOrd)
   module Set = Map.Set
 
   (* Alternative sets and maps indexed by the user part of the kernel names *)
 
-  module Map_env = HMap.Make(Ordered_env)
+  module Map_env = HMap.Make(UserOrd)
   module Set_env = Map_env.Set
 
 end
diff --git a/kernel/names.mli b/kernel/names.mli
index a0320fda43..76be6ca105 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -667,14 +667,14 @@ module GlobRef : sig
 
   val equal : t -> t -> bool
 
-  module Ordered : sig
+  module CanOrd : sig
     type nonrec t = t
     val compare : t -> t -> int
     val equal : t -> t -> bool
     val hash : t -> int
   end
 
-  module Ordered_env : sig
+  module UserOrd : sig
     type nonrec t = t
     val compare : t -> t -> int
     val equal : t -> t -> bool
diff --git a/library/coqlib.ml b/library/coqlib.ml
index 04a6e159eb..b374ecbca0 100644
--- a/library/coqlib.ml
+++ b/library/coqlib.ml
@@ -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/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml
index f13901c36d..4adad53899 100644
--- a/plugins/firstorder/instances.ml
+++ b/plugins/firstorder/instances.ml
@@ -38,7 +38,7 @@ let compare_gr id1 id2 =
   if id1==id2 then 0 else
     if id1==dummy_id then 1
     else if id2==dummy_id then -1
-    else GlobRef.Ordered.compare id1 id2
+    else GlobRef.CanOrd.compare id1 id2
 
 module OrderedInstance=
 struct
diff --git a/plugins/firstorder/sequent.ml b/plugins/firstorder/sequent.ml
index db3631daa4..99c5f85125 100644
--- a/plugins/firstorder/sequent.ml
+++ b/plugins/firstorder/sequent.ml
@@ -62,7 +62,7 @@ module Hitem=
 struct
   type t = h_item
   let compare (id1,co1) (id2,co2)=
-    let c = GlobRef.Ordered.compare id1 id2 in
+    let c = GlobRef.CanOrd.compare id1 id2 in
     if c = 0 then
       let cmp (i1, c1) (i2, c2) =
         let c = Int.compare i1 i2 in
diff --git a/pretyping/keys.ml b/pretyping/keys.ml
index 7a7099c195..dd3488c1df 100644
--- a/pretyping/keys.ml
+++ b/pretyping/keys.ml
@@ -34,7 +34,7 @@ module KeyOrdered = struct
 
   let hash gr =
     match gr with
-    | KGlob gr -> 9 + GlobRef.Ordered.hash gr
+    | KGlob gr -> 9 + GlobRef.CanOrd.hash gr
     | KLam -> 0
     | KLet -> 1
     | KProd -> 2
@@ -49,14 +49,14 @@ module KeyOrdered = struct
 
   let compare gr1 gr2 =
     match gr1, gr2 with
-    | KGlob gr1, KGlob gr2 -> GlobRef.Ordered.compare gr1 gr2
+    | KGlob gr1, KGlob gr2 -> GlobRef.CanOrd.compare gr1 gr2
     | _, KGlob _ -> -1
     | KGlob _, _ -> 1
     | k, k' -> Int.compare (hash k) (hash k')
 
   let equal k1 k2 =
     match k1, k2 with
-    | KGlob gr1, KGlob gr2 -> GlobRef.Ordered.equal gr1 gr2
+    | KGlob gr1, KGlob gr2 -> GlobRef.CanOrd.equal gr1 gr2
     | _, KGlob _ -> false
     | KGlob _, _ -> false
     | k, k' -> k == k'
diff --git a/printing/printer.ml b/printing/printer.ml
index bc26caefbe..be1cc0d64a 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -884,7 +884,7 @@ struct
       MutInd.CanOrd.compare m1 m2
     | Guarded k1 , Guarded k2
     | TypeInType k1, TypeInType k2 ->
-      GlobRef.Ordered.compare k1 k2
+      GlobRef.CanOrd.compare k1 k2
     | Constant _, _ -> -1
     | _, Constant _ -> 1
     | Positive _, _ -> -1
diff --git a/tactics/btermdn.ml b/tactics/btermdn.ml
index f721e9956b..af0ca22868 100644
--- a/tactics/btermdn.ml
+++ b/tactics/btermdn.ml
@@ -27,7 +27,7 @@ type term_label =
 | SortLabel
 
 let compare_term_label t1 t2 = match t1, t2 with
-| GRLabel gr1, GRLabel gr2 -> GlobRef.Ordered.compare gr1 gr2
+| GRLabel gr1, GRLabel gr2 -> GlobRef.CanOrd.compare gr1 gr2
 | _ -> pervasives_compare t1 t2 (** OK *)
 
 type 'res lookup_res = 'res Dn.lookup_res = Label of 'res | Nothing | Everything
diff --git a/tactics/term_dnet.ml b/tactics/term_dnet.ml
index 3bcd235b41..fee9dd1b96 100644
--- a/tactics/term_dnet.ml
+++ b/tactics/term_dnet.ml
@@ -107,7 +107,7 @@ struct
   | DRel, _ -> -1 | _, DRel -> 1
   | DSort, DSort -> 0
   | DSort, _ -> -1 | _, DSort -> 1
-  | DRef gr1, DRef gr2 -> GlobRef.Ordered.compare gr1 gr2
+  | DRef gr1, DRef gr2 -> GlobRef.CanOrd.compare gr1 gr2
   | DRef _, _ -> -1 | _, DRef _ -> 1
 
   | DCtx (tl1, tr1), DCtx (tl2, tr2)