diff options
| author | aspiwack | 2009-01-23 14:47:07 +0000 |
|---|---|---|
| committer | aspiwack | 2009-01-23 14:47:07 +0000 |
| commit | 9e40a64bc3f50fa6ec2b42b988b09bc5168eb7a0 (patch) | |
| tree | 1a4898cd173ab695a41699a73a427d74ad72d8f0 /toplevel | |
| parent | d47797d7c09d250fabd21330e665b02af3fa8639 (diff) | |
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
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/command.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/toplevel/command.ml b/toplevel/command.ml index 89739b9840..1ab819a5eb 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 |