From ec00fc09265f86b8cfd6bd6c7c72e20b35e7d436 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 4 Mar 2014 21:53:21 +0100
Subject: Adding a CSet module in Coq lib.

---
 lib/cSet.mli | 31 +++++++++++++++++++++++++++++++
 1 file changed, 31 insertions(+)
 create mode 100644 lib/cSet.mli

(limited to 'lib/cSet.mli')

diff --git a/lib/cSet.mli b/lib/cSet.mli
new file mode 100644
index 0000000000..77381d0a84
--- /dev/null
+++ b/lib/cSet.mli
@@ -0,0 +1,31 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+module type OrderedType =
+sig
+  type t
+  val compare : t -> t -> int
+end
+
+module type S = Set.S
+
+module Make(M : OrderedType) : S
+  with type elt = M.t
+  and type t = Set.Make(M).t
+
+module type HashedType =
+sig
+  type t
+  val hash : t -> int
+end
+
+module Hashcons (M : OrderedType) (H : HashedType with type t = M.t) : Hashcons.S with
+  type t = Set.Make(M).t
+  and type u = M.t -> M.t
+(** Create hash-consing for sets. The hashing function provided must be
+    compatible with the comparison function. *)
-- 
cgit v1.2.3