From bb5e6d7c39211349d460db0b61b2caf3d099d5b6 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Wed, 23 Oct 2013 22:17:33 +0000
Subject: cList: a few alternative to hashtbl-based uniquize, distinct, subset

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16924 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/names.ml  | 12 +++++++++---
 kernel/names.mli |  3 +++
 2 files changed, 12 insertions(+), 3 deletions(-)

(limited to 'kernel')

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. *)
 
-- 
cgit v1.2.3