From 9e40a64bc3f50fa6ec2b42b988b09bc5168eb7a0 Mon Sep 17 00:00:00 2001
From: aspiwack
Date: Fri, 23 Jan 2009 14:47:07 +0000
Subject: 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
---
 contrib/extraction/extract_env.ml  | 2 +-
 contrib/subtac/subtac_pretyping.ml | 7 -------
 2 files changed, 1 insertion(+), 8 deletions(-)

(limited to 'contrib')

diff --git a/contrib/extraction/extract_env.ml b/contrib/extraction/extract_env.ml
index 831f31b188..39e2770819 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 f65e3f786d..0159de5427 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
-- 
cgit v1.2.3