aboutsummaryrefslogtreecommitdiff
path: root/doc/RecTutorial
diff options
context:
space:
mode:
authoraspiwack2009-01-23 14:47:07 +0000
committeraspiwack2009-01-23 14:47:07 +0000
commit9e40a64bc3f50fa6ec2b42b988b09bc5168eb7a0 (patch)
tree1a4898cd173ab695a41699a73a427d74ad72d8f0 /doc/RecTutorial
parentd47797d7c09d250fabd21330e665b02af3fa8639 (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 'doc/RecTutorial')
0 files changed, 0 insertions, 0 deletions