- documentation repertoire proofs/

 - IsAppL of constr * constr list ==> répercussion
 - module Clenv (suite; as terminé)


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@113 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 16 insertions, 0 deletions

diff --git a/lib/util.ml b/lib/util.ml
index 62a86b55f5..0206bf887d 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -278,8 +278,17 @@ type ('a,'b) union = Inl of 'a | Inr of 'b
 
 module Intset = Set.Make(struct type t = int let compare = compare end)
 
+let intset_exists p s = Intset.fold (fun x b -> (p x) || b) s false
+
 module Intmap = Map.Make(struct type t = int let compare = compare end)
 
+let intmap_in_dom x m =
+  try let _ = Intmap.find x m in true with Not_found -> false
+
+let intmap_to_list m = Intmap.fold (fun n v l -> (n,v)::l) m []
+
+let intmap_inv m b = Intmap.fold (fun n v l -> if v = b then n::l else l) m []
+
 let out_some = function
   | Some x -> x
   | None -> failwith "out_some"
diff --git a/lib/util.mli b/lib/util.mli
index 4075a70451..6f1e258727 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -78,8 +78,15 @@ val repeat : int -> ('a -> unit) -> 'a -> unit
 type ('a,'b) union = Inl of 'a | Inr of 'b
 
 module Intset : Set.S with type elt = int
+
+val intset_exists : (int -> bool) -> Intset.t -> bool
+
 module Intmap : Map.S with type key = int
 
+val intmap_in_dom : int -> 'a Intmap.t -> bool
+val intmap_to_list : 'a Intmap.t -> (int * 'a) list
+val intmap_inv : 'a Intmap.t -> 'a -> int list
+
 val out_some : 'a option -> 'a
 val option_app : ('a -> 'b) -> 'a option -> 'b option