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

1 files changed, 1 insertions, 8 deletions

diff --git a/library/impargs.ml b/library/impargs.ml
index b477d94958..be872d303f 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 =