diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-04-16 14:13:00 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-04-16 14:13:00 +0000 |
| commit | e960cd8dac76829f3a48167e70a23c65d8dd797f (patch) | |
| tree | 6a4612192d654046872255f98bacf984da949288 /lib/util.mli | |
| parent | f57a38bb53dc06cef1cee78c60946aa5e6d3cf0b (diff) | |
Util: remove list_split_at which is a clone of list_chop
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12939 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'lib/util.mli')
| -rw-r--r-- | lib/util.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/lib/util.mli b/lib/util.mli index ddf32e762..f900e9bf7 100644 --- a/lib/util.mli +++ b/lib/util.mli @@ -116,7 +116,6 @@ val list_union : 'a list -> 'a list -> 'a list val list_unionq : 'a list -> 'a list -> 'a list val list_subtract : 'a list -> 'a list -> 'a list val list_subtractq : 'a list -> 'a list -> 'a list -val list_chop : int -> 'a list -> 'a list * 'a list (* [list_tabulate f n] builds [[f 0; ...; f (n-1)]] *) val list_tabulate : (int -> 'a) -> int -> 'a list val list_make : int -> 'a -> 'a list @@ -164,7 +163,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 : int -> 'a list -> 'a list*'a list +val list_chop : int -> 'a list -> 'a list * 'a list +(* former [list_split_at] was a duplicate of [list_chop] *) 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 |