4 files changed, 22 insertions, 8 deletions
diff --git a/library/globnames.ml b/library/globnames.ml
index 7fce6b378..8a9e99621 100644
--- a/library/globnames.ml
+++ b/library/globnames.ml
@@ -77,6 +77,15 @@ let constr_of_global = function
 let constr_of_reference = constr_of_global
 let reference_of_constr = global_of_constr
 
+let global_eq_gen eq_cst eq_ind eq_cons x y =
+  x == y ||
+  match x, y with
+  | ConstRef cx, ConstRef cy -> eq_cst cx cy
+  | IndRef indx, IndRef indy -> eq_ind indx indy
+  | ConstructRef consx, ConstructRef consy -> eq_cons consx consy
+  | VarRef v1, VarRef v2 -> Id.equal v1 v2
+  | (VarRef _ | ConstRef _ | IndRef _ | ConstructRef _), _ -> false
+
 let global_ord_gen ord_cst ord_ind ord_cons x y =
   if x == y then 0
   else match x, y with
@@ -107,6 +116,7 @@ module RefOrdered = struct
   type t = global_reference
   let compare gr1 gr2 =
     global_ord_gen compare ind_ord constructor_ord gr1 gr2
+  let equal gr1 gr2 = global_eq_gen equal eq_ind eq_constructor gr1 gr2
   let hash gr = global_hash_gen hash ind_hash constructor_hash gr
 end
 
@@ -115,6 +125,8 @@ module RefOrdered_env = struct
   type t = global_reference
   let compare gr1 gr2 =
     global_ord_gen compare ind_user_ord constructor_user_ord gr1 gr2
+  let equal gr1 gr2 =
+    global_eq_gen equal eq_user_ind eq_user_constructor gr1 gr2
   let hash gr = global_hash_gen hash ind_user_hash constructor_user_hash gr
 end
 
@@ -140,6 +152,13 @@ type extended_global_reference =
 module ExtRefOrdered = struct
   type t = extended_global_reference
 
+  let equal x y =
+    x == y ||
+    match x, y with
+    | TrueGlobal rx, TrueGlobal ry -> RefOrdered_env.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
diff --git a/library/globnames.mli b/library/globnames.mli
index 4569d8e1f..0a7bf850c 100644
--- a/library/globnames.mli
+++ b/library/globnames.mli
@@ -77,6 +77,7 @@ type extended_global_reference =
 module ExtRefOrdered : sig
   type t = extended_global_reference
   val compare : t -> t -> int
+  val equal : t -> t -> bool
   val hash : t -> int
 end
 
diff --git a/library/libnames.ml b/library/libnames.ml
index cf6d4c8ad..97c352d61 100644
--- a/library/libnames.ml
+++ b/library/libnames.ml
@@ -105,7 +105,7 @@ let string_of_path sp =
 let sp_ord sp1 sp2 =
   let (p1,id1) = repr_path sp1
   and (p2,id2) = repr_path sp2 in
-  let p_bit = compare p1 p2 in
+  let p_bit = DirPath.compare p1 p2 in
   if Int.equal p_bit 0 then Id.compare id1 id2 else p_bit
 
 module SpOrdered =
diff --git a/library/nametab.ml b/library/nametab.ml
index 08eb02c9d..03856736d 100644
--- a/library/nametab.ml
+++ b/library/nametab.ml
@@ -276,14 +276,8 @@ struct
       id, (DirPath.repr dir)
 end
 
-module ExtRefEqual =
-struct
-  type t = extended_global_reference
-  let equal e1 e2 = Int.equal (ExtRefOrdered.compare e1 e2) 0
-end
-
+module ExtRefEqual = ExtRefOrdered
 module KnEqual = Names.KerName
-
 module MPEqual = Names.ModPath
 
 module ExtRefTab = Make(FullPath)(ExtRefEqual)