diff options
| author |  pboutill <pboutill@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-02-11 11:06:05 +0000 |
|---|---|---|
| committer | pboutill <pboutill@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-02-11 11:06:05 +0000 |
| commit | 12ca03ff230adb011e7b10acd6645e97374f1c65 (patch) | |
| tree | 1473f174ba8ce56bdb07b41aff590981c0bae793 /kernel/names.mli | |
| 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/names.mli')
| -rw-r--r-- | kernel/names.mli | 7 |
1 files changed, 5 insertions, 2 deletions
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 |