- 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

1 files changed, 9 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"