2 files changed, 12 insertions, 3 deletions
diff --git a/kernel/names.ml b/kernel/names.ml
index 2a04ff3c55..00b8df4862 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -71,10 +71,16 @@ module Name =
 struct
   type t = Name of Id.t | Anonymous
 
+  let compare n1 n2 = match n1, n2 with
+    | Anonymous, Anonymous -> 0
+    | Name id1, Name id2 -> Id.compare id1 id2
+    | Anonymous, Name _ -> -1
+    | Name _, Anonymous -> 1
+
   let equal n1 n2 = match n1, n2 with
-  | Anonymous, Anonymous -> true
-  | Name id1, Name id2 -> String.equal id1 id2
-  | _ -> false
+    | Anonymous, Anonymous -> true
+    | Name id1, Name id2 -> String.equal id1 id2
+    | _ -> false
 
   module Self_Hashcons =
     struct
diff --git a/kernel/names.mli b/kernel/names.mli
index 82df075626..6f4ac9a530 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -53,6 +53,9 @@ sig
   type t = Name of Id.t | Anonymous
   (** A name is either undefined, either an identifier. *)
 
+  val compare : t -> t -> int
+  (** Comparison over names. *)
+
   val equal : t -> t -> bool
   (** Equality over names. *)