- Correction de la version simplifiée (filtrage sur deux sig

  imbriqués) du bug 1834, mais le bug 1834 reste ouvert [cases.ml].
- Réactivation de l'interprétation des listes dans "generalize" cassée
  depuis 11072) [tacinterp.ml].
- Bricoles et petit nettoyage en passant [cases.ml et g_vernac.ml4].


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

2 files changed, 13 insertions, 0 deletions

diff --git a/lib/util.ml b/lib/util.ml
index 4089dc03d..14a40e378 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -485,6 +485,11 @@ let list_tabulate f len =
   in 
   tabrec 0
 
+let rec list_make n v =
+  if n = 0 then []
+  else if n < 0 then invalid_arg "list_make"
+  else v::list_make (n-1) v
+
 let list_assign l n e = 
   let rec assrec stk = function
     | ((h::t), 0) -> List.rev_append stk (e::t)
@@ -700,6 +705,12 @@ let rec list_filter2 f = function
       if f d l then d::dp', l::lp' else p
   | _ -> invalid_arg "list_filter2"
 
+let rec list_map_filter f = function
+  | [] -> []
+  | x::l ->
+      let l' = list_map_filter f l in
+      match f x with None -> l' | Some y -> y::l'
+
 let list_subset l1 l2 =
   let t2 = Hashtbl.create 151 in
   List.iter (fun x -> Hashtbl.add t2 x ()) l2;
diff --git a/lib/util.mli b/lib/util.mli
index bc1a9cc26..9c0756fc9 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -103,10 +103,12 @@ val list_subtractq : 'a list -> 'a list -> 'a list
 val list_chop : int -> 'a list -> 'a list * 'a list
 (* [list_tabulate f n] builds [[f 0; ...; f (n-1)]] *)
 val list_tabulate : (int -> 'a) -> int -> 'a list
+val list_make : int -> 'a -> 'a list
 val list_assign : 'a list -> int -> 'a -> 'a list
 val list_distinct : 'a list -> bool
 val list_duplicates : 'a list -> 'a list
 val list_filter2 : ('a -> 'b -> bool) -> 'a list * 'b list -> 'a list * 'b list
+val list_map_filter : ('a -> 'b option) -> 'a list -> 'b list
 (* [list_smartmap f [a1...an] = List.map f [a1...an]] but if for all i
    [ f ai == ai], then [list_smartmap f l==l] *)
 val list_smartmap : ('a -> 'a) -> 'a list -> 'a list