diff options
Diffstat (limited to 'lib/cMap.mli')
-rw-r--r-- | lib/cMap.mli | 35 |
1 files changed, 35 insertions, 0 deletions
diff --git a/lib/cMap.mli b/lib/cMap.mli new file mode 100644 index 000000000..9b7043d9e --- /dev/null +++ b/lib/cMap.mli @@ -0,0 +1,35 @@ +(************************************************************************) +(* 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 *) +(************************************************************************) + +(** {5 Extended version of OCaml's maps} *) + +module type OrderedType = +sig + type t + val compare : t -> t -> int +end + +module type S = Map.S + +module type ExtS = +sig + include Map.S + (** The underlying Map library *) + + module Set : Set.S with type elt = key + (** Sets used by the domain function *) + + val domain : 'a t -> Set.t + (** Recover the set of keys defined in the map. *) + +end + +module Make(M : Map.OrderedType) : ExtS with + type key = M.t + and type 'a t = 'a Map.Make(M).t + and module Set := Set.Make(M) |