diff options
author | 2011-02-11 11:06:05 +0000 | |
---|---|---|
committer | 2011-02-11 11:06:05 +0000 | |
commit | 12ca03ff230adb011e7b10acd6645e97374f1c65 (patch) | |
tree | 1473f174ba8ce56bdb07b41aff590981c0bae793 /kernel | |
parent | 2d8c70b3380d899c2717d00f2f27b4c6aefa2322 (diff) |
compatibility <3.12 (Map.exists Map.singleton)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13829 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel')
-rw-r--r-- | kernel/names.ml | 10 | ||||
-rw-r--r-- | kernel/names.mli | 7 |
2 files changed, 14 insertions, 3 deletions
diff --git a/kernel/names.ml b/kernel/names.ml index d53a7aa30..6e39b35bb 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -48,7 +48,15 @@ module IdOrdered = end module Idset = Set.Make(IdOrdered) -module Idmap = Map.Make(IdOrdered) +module Idmap = +struct + include Map.Make(IdOrdered) + exception Finded + let exists f m = + try iter (fun a b -> if f a b then raise Finded) m ; false + with |Finded -> true + let singleton k v = add k v empty +end module Idpred = Predicate.Make(IdOrdered) (* Names *) diff --git a/kernel/names.mli b/kernel/names.mli index bf1fca87f..2d112b32a 100644 --- a/kernel/names.mli +++ b/kernel/names.mli @@ -20,8 +20,11 @@ val id_ord : identifier -> identifier -> int (** Identifiers sets and maps *) module Idset : Set.S with type elt = identifier module Idpred : Predicate.S with type elt = identifier -module Idmap : Map.S with type key = identifier - +module Idmap : sig + include Map.S with type key = identifier + val exists : (identifier -> 'a -> bool) -> 'a t -> bool + val singleton : key -> 'a -> 'a t +end (** {6 Directory paths = section names paths } *) type module_ident = identifier module ModIdmap : Map.S with type key = module_ident |