Merge with lmamane's private branch:

 - New vernac command "Delete"
 - New vernac command "Undo To"
 - Added a few hooks used by new contrib/interface
 - Beta/incomplete version of dependency generation and dumping


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

2 files changed, 20 insertions, 0 deletions

diff --git a/lib/util.ml b/lib/util.ml
index 5e3f7fa6bf..29edaf3073 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -486,6 +486,18 @@ let list_fold_map' f l e =
 
 let list_map_assoc f = List.map (fun (x,a) -> (x,f a))
 
+(* Specification:
+   - =p= is set equality (double inclusion)
+   - f such that \forall l acc, (f l acc) =p= append (f l []) acc
+   - let g = fun x -> f x [] in
+   - union_map f l acc =p= append (flatten (map g l)) acc
+ *)
+let list_union_map f l acc =
+  List.fold_left
+    (fun x y -> f y x)
+    acc
+    l
+
 (* A generic cartesian product: for any operator (**), 
    [list_cartesian (**) [x1;x2] [y1;y2] = [x1**y1; x1**y2; x2**y1; x2**y1]], 
    and so on if there are more elements in the lists. *)
@@ -761,6 +773,12 @@ let array_distinct v =
   with Exit ->
     false
 
+let array_union_map f a acc =
+  Array.fold_left
+    (fun x y -> f y x)
+    acc
+    a
+
 (* Matrices *)
 
 let matrix_transpose mat =
diff --git a/lib/util.mli b/lib/util.mli
index ae1b906ce1..92822f770b 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -159,6 +159,7 @@ val list_cartesians : ('a -> 'b -> 'b) -> 'b -> 'a list list -> 'b list
 (* list_combinations [[a;b];[c;d]] returns [[a;c];[a;d];[b;c];[b;d]] *)
 val list_combinations : 'a list list -> 'a list list
 
+val list_union_map : ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b
 
 (*s Arrays. *)
 
@@ -201,6 +202,7 @@ val array_fold_map' : ('a -> 'c -> 'b * 'c) -> 'a array -> 'c -> 'b array * 'c
 val array_fold_map2' :
   ('a -> 'b -> 'c -> 'd * 'c) -> 'a array -> 'b array -> 'c -> 'd array * 'c
 val array_distinct : 'a array -> bool
+val array_union_map : ('a -> 'b -> 'b) -> 'a array -> 'b -> 'b
 
 (*s Matrices *)