Petit nettoyage faisant suite au commit #11847 .

Quelques modifications autour (géographiquement) de Util.list_split_at

Util.list_split_at devient Util.list_split_when (dénomination inventée
arbitrairement par moi-même, mais qui ne devrait pas déranger grand
monde vu qu'il semble n'y avoir que deux occurences de cette fonction).
Pour laisser la place à la fonction suivante :

Introduction de Util.list_split_at: qui sépare la liste à une position
donnée (alors que la nouvellement nommé list_split_when sépare à la 
première occurence "vrai" d'un prédicat).                            

Ajout de quelques commentaires dans util.ml (pas le mli) sur ces deux 
fonctions.

Suppression de Impargs.list_split_at (appel à Util).   

Suppression de Subtac_pretyping.list_split_at (qui était du code mort de 
toute façon).

Suppression Util.list_split_by qui n'est utilisé nulle part et est une 
réimplémentation de List.partition (qui est probablement meilleure, en 
particulier tail-recursive)



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

7 files changed, 23 insertions, 32 deletions

diff --git a/contrib/extraction/extract_env.ml b/contrib/extraction/extract_env.ml
index 831f31b18..39e277081 100644
--- a/contrib/extraction/extract_env.ml
+++ b/contrib/extraction/extract_env.ml
@@ -161,7 +161,7 @@ let env_for_mtb_with env mtb idl =
     | _ -> assert false
   in
   let l = label_of_id (List.hd idl) in
-  let before = fst (list_split_at (fun (l',_) -> l=l') sig_b) in
+  let before = fst (list_split_when (fun (l',_) -> l=l') sig_b) in
   Modops.add_signature (MPself msid) before env
 
 (* From a [structure_body] (i.e. a list of [structure_field_body])
diff --git a/contrib/subtac/subtac_pretyping.ml b/contrib/subtac/subtac_pretyping.ml
index f65e3f786..0159de542 100644
--- a/contrib/subtac/subtac_pretyping.ml
+++ b/contrib/subtac/subtac_pretyping.ml
@@ -84,13 +84,6 @@ let find_with_index x l =
     | [] -> raise Not_found
   in aux 0 l
 
-let list_split_at index l = 
-  let rec aux i acc = function
-      hd :: tl when i = index -> (List.rev acc), tl
-    | hd :: tl -> aux (succ i) (hd :: acc) tl
-    | [] -> failwith "list_split_at: Invalid argument"
-  in aux 0 [] l
-
 open Vernacexpr
 
 let coqintern_constr evd env : Topconstr.constr_expr -> Rawterm.rawconstr = Constrintern.intern_constr (evars_of evd) env
diff --git a/lib/util.ml b/lib/util.ml
index c685ee226..172d8d911 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -770,21 +770,26 @@ let list_subset l1 l2 =
   in 
   look l1
 
-let list_split_at p = 
-  let rec split_at_loop x y = 
+(* [list_split_at i l] splits [l] into two lists [(l1,l2)] such that [l1++l2=l] 
+    and [l1] has length [i].
+    It raises [Failure] when [i] is negative or greater than the length of [l]  *)
+let list_split_at index l = 
+  let rec aux i acc = function
+      tl when i = index -> (List.rev acc), tl
+    | hd :: tl -> aux (succ i) (hd :: acc) tl
+    | [] -> failwith "list_split_at: Invalid argument"
+  in aux 0 [] l
+
+(* [list_split_when p l] splits [l] into two lists [(l1,a::l2)] such that
+    [l1++(a::l2)=l], [p a=true] and [p b = false] for every element [b] of [l1].
+    If there is no such [a], then it returns [(l,[])] instead *)
+let list_split_when p = 
+  let rec split_when_loop x y = 
     match y with 
       | []      -> ([],[])
-      | (a::l)  -> if (p a) then (List.rev x,y) else split_at_loop (a::x) l
+      | (a::l)  -> if (p a) then (List.rev x,y) else split_when_loop (a::x) l
   in 
-  split_at_loop []
-
-let list_split_by p = 
-  let rec split_loop = function
-  | []      -> ([],[])
-  | (a::l)  ->
-      let (l1,l2) = split_loop l in if (p a) then (a::l1,l2) else (l1,a::l2)
-  in 
-  split_loop
+  split_when_loop []
 
 let rec list_split3 = function
   | [] -> ([], [], [])
diff --git a/lib/util.mli b/lib/util.mli
index 7af5816ea..023b8a15e 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -150,8 +150,8 @@ val list_uniquize : 'a list -> 'a list
 (* merges two sorted lists and preserves the uniqueness property: *)
 val list_merge_uniq : ('a -> 'a -> int) -> 'a list -> 'a list -> 'a list
 val list_subset : 'a list -> 'a list -> bool
-val list_split_at : ('a -> bool) -> 'a list -> 'a list * 'a list
-val list_split_by : ('a -> bool) -> 'a list -> 'a list * 'a list
+val list_split_at : int -> 'a list -> 'a list*'a list
+val list_split_when : ('a -> bool) -> 'a list -> 'a list * 'a list
 val list_split3 : ('a * 'b * 'c) list -> 'a list * 'b list * 'c list
 val list_partition_by : ('a -> 'a -> bool) -> 'a list -> 'a list list
 val list_firstn : int -> 'a list -> 'a list
diff --git a/library/impargs.ml b/library/impargs.ml
index b477d9495..be872d303 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -35,7 +35,7 @@ type implicits_flags = {
   maximal : bool
 }
 
-(* les implicites sont stricts par défaut en v8 *)
+(* les implicites sont stricts par défaut en v8 *)
 
 let implicit_args = ref { 
   main = false;
@@ -415,13 +415,6 @@ let compute_global_implicits flags manual = function
       let (_,cimps) = (compute_mib_implicits flags manual kn).(i) in snd cimps.(j-1)
 
 (* Merge a manual explicitation with an implicit_status list *)
-
-let list_split_at index l = 
-  let rec aux i acc = function
-      tl when i = index -> (List.rev acc), tl
-    | hd :: tl -> aux (succ i) (hd :: acc) tl
-    | [] -> failwith "list_split_at: Invalid argument"
-  in aux 0 [] l
     
 let merge_impls oldimpls newimpls =
   let (before, news), olds = 
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 6bded84dd..3cef0ef2e 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -213,7 +213,7 @@ let onHyps find tac gl = tac (find gl) gl
    after id *)
 
 let afterHyp id gl =
-  fst (list_split_at (fun (hyp,_,_) -> hyp = id) (pf_hyps gl))
+  fst (list_split_when (fun (hyp,_,_) -> hyp = id) (pf_hyps gl))
     
 
 (* Create a singleton clause list with the last hypothesis from then context *)
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 89739b984..1ab819a5e 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -1007,7 +1007,7 @@ let list_split_rev_at index l =
   let rec aux i acc = function
       hd :: tl when i = index -> acc, tl
     | hd :: tl -> aux (succ i) (hd :: acc) tl
-    | [] -> failwith "list_split_at: Invalid argument"
+    | [] -> failwith "list_split_when: Invalid argument"
   in aux 0 [] l
 
 let fold_left' f = function