Auto,Dhyp,Elim / Reduction de Evar / declarations eliminations

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

2 files changed, 18 insertions, 2 deletions

diff --git a/lib/util.ml b/lib/util.ml
index 7f726fe0ed..d165c157b2 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -51,6 +51,10 @@ let parse_section_path s =
 
 module Stringmap = Map.Make(struct type t = string let compare = compare end)
 
+let stringmap_to_list m = Stringmap.fold (fun s y l -> (s,y)::l) m []
+
+let stringmap_dom m = Stringmap.fold (fun s _ l -> s::l) m []
+
 (* Lists *)
 
 let list_intersect l1 l2 = 
@@ -189,7 +193,12 @@ let list_prefix_of prefl l =
     | (_, _) -> false
   in 
   prefrec (prefl,l)
-    
+
+let list_map_append f l = List.flatten (List.map f l)
+
+let list_map_append2 f l1 l2 = List.flatten (List.map2 f l1 l2)
+
+
 (* Arrays *)
 
 let array_exists f v = 
diff --git a/lib/util.mli b/lib/util.mli
index 77c87c5288..bcdf4493c6 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -28,6 +28,9 @@ val parse_section_path : string -> string list * string * string
 
 module Stringmap : Map.S with type key = string
 
+val stringmap_to_list : 'a Stringmap.t -> (string * 'a) list 
+val stringmap_dom : 'a Stringmap.t -> string list
+
 (*s Lists. *)
 
 val list_intersect : 'a list -> 'a list -> 'a list
@@ -54,6 +57,10 @@ val list_splitby : ('a -> bool) -> 'a list -> 'a list * 'a list
 val list_firstn : int -> 'a list -> 'a list
 val list_lastn : int -> 'a list -> 'a list
 val list_prefix_of : 'a list -> 'a list -> bool
+(* [map_append f [x1; ...; xn]] returns [(f x1)@(f x2)@...@(f xn)] *)
+val list_map_append : ('a -> 'b list) -> 'a list -> 'b list
+(* raises [Invalid_argument] if the two lists don't have the same length *)
+val list_map_append2 : ('a -> 'b -> 'c list) -> 'a list -> 'b list -> 'c list
 
 (*s Arrays. *)
 
@@ -72,7 +79,7 @@ val array_fold_left_from : int -> ('a -> 'b -> 'a) -> 'a -> 'b array -> 'a
 val array_fold_right_from : int -> ('a -> 'b -> 'b) -> 'a array -> 'b -> 'b
 val array_app_tl : 'a array -> 'a list -> 'a list
 val array_list_of_tl : 'a array -> 'a list
-val array_map_to_list : ('a -> 'b) -> 'a array ->'b list
+val array_map_to_list : ('a -> 'b) -> 'a array -> 'b list
 val array_chop : int -> 'a array -> 'a array * 'a array
 val array_map2 : ('a -> 'b -> 'c) -> 'a array -> 'b array -> 'c array
 val array_map3 :