Cleaning, documentation, uniformisation of the Coq extension of List.

Still some discrepancies though. E.g.:
- some functions taking an equality as arguments have suffix `_f` but
  not all;
- the functions possibly raising an error have still different kinds
  of failure (Failure, Invalid_argument, Not_found or IndexOutOfRange,
  and when in the first two cases, with no unique rules in the style
  of the associated string - we thus avoid to document the exact
  string used).

There are a few semantics changes:
- skipn_at_least now raises a `Failure` if its argument is negative;
- map3 raises an Invalid_argument "List.map3" rather than
  Invalid_argument "map3" and similarly for map4
- internally, map3 and map4 are now tail-recursive (by uniformity);
- internally, split3 and combine3 are now tail-recursive (by uniformity);
- filter is now "smart" by default and smartfilter is deprecated;
- smartmap is now tail-recursive by default.

2 files changed, 866 insertions, 640 deletions

diff --git a/clib/cList.ml b/clib/cList.ml
index 7621793d4..a580900e6 100644
--- a/clib/cList.ml
+++ b/clib/cList.ml
@@ -19,25 +19,31 @@ sig
   val compare : 'a cmp -> 'a list cmp
   val equal : 'a eq -> 'a list eq
   val is_empty : 'a list -> bool
-  val init : int -> (int -> 'a) -> 'a list
   val mem_f : 'a eq -> 'a -> 'a list -> bool
-  val add_set : 'a eq -> 'a -> 'a list -> 'a list
-  val eq_set : 'a eq -> 'a list -> 'a list -> bool
-  val intersect : 'a eq -> 'a list -> 'a list -> 'a list
-  val union : 'a eq -> 'a list -> 'a list -> 'a list
-  val unionq : 'a list -> 'a list -> 'a list
-  val subtract : 'a eq -> 'a list -> 'a list -> 'a list
-  val subtractq : 'a list -> 'a list -> 'a list
+  val for_all_i : (int -> 'a -> bool) -> int -> 'a list -> bool
+  val for_all2eq : ('a -> 'b -> bool) -> 'a list -> 'b list -> bool
+  val prefix_of : 'a eq -> 'a list -> 'a list -> bool
   val interval : int -> int -> int list
   val make : int -> 'a -> 'a list
+  val addn : int -> 'a -> 'a list -> 'a list
+  val init : int -> (int -> 'a) -> 'a list
+  val append : 'a list -> 'a list -> 'a list
+  val concat : 'a list list -> 'a list
+  val flatten : 'a list list -> 'a list
   val assign : 'a list -> int -> 'a -> 'a list
-  val distinct : 'a list -> bool
-  val distinct_f : 'a cmp -> 'a list -> bool
-  val duplicates : 'a eq -> 'a list -> 'a list
+  val filter : ('a -> bool) -> 'a list -> 'a list
   val filter2 : ('a -> 'b -> bool) -> 'a list -> 'b list -> 'a list * 'b list
+  val filteri :
+    (int -> 'a -> bool) -> 'a list -> 'a list
+  val filter_with : bool list -> 'a list -> 'a list
+  val smartfilter : ('a -> bool) -> 'a list -> 'a list
+  [@@ocaml.deprecated "Same as [filter]"]
   val map_filter : ('a -> 'b option) -> 'a list -> 'b list
   val map_filter_i : (int -> 'a -> 'b option) -> 'a list -> 'b list
-  val filter_with : bool list -> 'a list -> 'a list
+  val partitioni :
+    (int -> 'a -> bool) -> 'a list -> 'a list * 'a list
+  val map : ('a -> 'b) -> 'a list -> 'b list
+  val map2 : ('a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list
   val smartmap : ('a -> 'a) -> 'a list -> 'a list
   [@@ocaml.deprecated "Same as [Smart.map]"]
   val map_left : ('a -> 'b) -> 'a list -> 'b list
@@ -48,18 +54,13 @@ sig
     ('a -> 'b -> 'c -> 'd) -> 'a list -> 'b list -> 'c list -> 'd list
   val map4 :
     ('a -> 'b -> 'c -> 'd -> 'e) -> 'a list -> 'b list -> 'c list -> 'd list -> 'e list
-  val filteri :
-    (int -> 'a -> bool) -> 'a list -> 'a list
-  val partitioni :
-    (int -> 'a -> bool) -> 'a list -> 'a list * 'a list
   val map_of_array : ('a -> 'b) -> 'a array -> 'b list
-  val smartfilter : ('a -> bool) -> 'a list -> 'a list
-  [@@ocaml.deprecated "Same as [Smart.map]"]
+  val map_append : ('a -> 'b list) -> 'a list -> 'b list
+  val map_append2 : ('a -> 'b -> 'c list) -> 'a list -> 'b list -> 'c list
   val extend : bool list -> 'a -> 'a list -> 'a list
   val count : ('a -> bool) -> 'a list -> int
   val index : 'a eq -> 'a -> 'a list -> int
   val index0 : 'a eq -> 'a -> 'a list -> int
-  val iteri :  (int -> 'a -> unit) -> 'a list -> unit
   val fold_left_until : ('c -> 'a -> 'c CSig.until) -> 'c -> 'a list -> 'c
   val fold_right_i :  (int -> 'a -> 'b -> 'b) -> int -> 'a list -> 'b -> 'b
   val fold_left_i :  (int -> 'a -> 'b -> 'a) -> int -> 'a -> 'b list -> 'a
@@ -67,62 +68,68 @@ sig
       ('a -> 'b -> 'b list -> 'a) -> 'b list -> 'a -> 'a
   val fold_left3 : ('a -> 'b -> 'c -> 'd -> 'a) -> 'a -> 'b list -> 'c list -> 'd list -> 'a
   val fold_left2_set : exn -> ('a -> 'b -> 'c -> 'b list -> 'c list -> 'a) -> 'a -> 'b list -> 'c list -> 'a
-  val for_all_i : (int -> 'a -> bool) -> int -> 'a list -> bool
+  val fold_left_map : ('a -> 'b -> 'a * 'c) -> 'a -> 'b list -> 'a * 'c list
+  val fold_right_map : ('b -> 'a -> 'c * 'a) -> 'b list -> 'a -> 'c list * 'a
+  val fold_left2_map : ('a -> 'b -> 'c -> 'a * 'd) -> 'a -> 'b list -> 'c list -> 'a * 'd list
+  val fold_right2_map : ('b -> 'c -> 'a -> 'd * 'a) -> 'b list -> 'c list -> 'a -> 'd list * 'a
+  val fold_left3_map : ('a -> 'b -> 'c -> 'd -> 'a * 'e) -> 'a -> 'b list -> 'c list -> 'd list -> 'a * 'e list
+  val fold_left4_map : ('a -> 'b -> 'c -> 'd -> 'e -> 'a * 'r) -> 'a -> 'b list -> 'c list -> 'd list -> 'e list -> 'a * 'r list
+  val fold_map : ('a -> 'b -> 'a * 'c) -> 'a -> 'b list -> 'a * 'c list
+  [@@ocaml.deprecated "Same as [fold_left_map]"]
+  val fold_map' : ('b -> 'a -> 'c * 'a) -> 'b list -> 'a -> 'c list * 'a
+  [@@ocaml.deprecated "Same as [fold_right_map]"]
   val except : 'a eq -> 'a -> 'a list -> 'a list
   val remove : 'a eq -> 'a -> 'a list -> 'a list
   val remove_first : ('a -> bool) -> 'a list -> 'a list
   val extract_first : ('a -> bool) -> 'a list -> 'a list * 'a
-  val insert : ('a -> 'a -> bool) -> 'a -> 'a list -> 'a list
-  val for_all2eq : ('a -> 'b -> bool) -> 'a list -> 'b list -> bool
-  val sep_last : 'a list -> 'a * 'a list
   val find_map : ('a -> 'b option) -> 'a list -> 'b
-  val uniquize : 'a list -> 'a list
-  val sort_uniquize : 'a cmp -> 'a list -> 'a list
-  val merge_uniq : ('a -> 'a -> int) -> 'a list -> 'a list -> 'a list
-  val subset : 'a list -> 'a list -> bool
-  val chop : int -> 'a list -> 'a list * 'a list
   exception IndexOutOfRange
   val goto : int -> 'a list -> 'a list * 'a list
   val split_when : ('a -> bool) -> 'a list -> 'a list * 'a list
-  val split3 : ('a * 'b * 'c) list -> 'a list * 'b list * 'c list
-  val firstn : int -> 'a list -> 'a list
+  val sep_last : 'a list -> 'a * 'a list
+  val drop_last : 'a list -> 'a list
   val last : 'a list -> 'a
   val lastn : int -> 'a list -> 'a list
+  val chop : int -> 'a list -> 'a list * 'a list
+  val firstn : int -> 'a list -> 'a list
   val skipn : int -> 'a list -> 'a list
   val skipn_at_least : int -> 'a list -> 'a list
-  val addn : int -> 'a -> 'a list -> 'a list
-  val prefix_of : 'a eq -> 'a list -> 'a list -> bool
   val drop_prefix : 'a eq -> 'a list -> 'a list -> 'a list
-  val drop_last : 'a list -> 'a list
-  val map_append : ('a -> 'b list) -> 'a list -> 'b list
-  val map_append2 : ('a -> 'b -> 'c list) -> 'a list -> 'b list -> 'c list
+  val insert : ('a -> 'a -> bool) -> 'a -> 'a list -> 'a list
   val share_tails : 'a list -> 'a list -> 'a list * 'a list * 'a list
-  val fold_left_map : ('a -> 'b -> 'a * 'c) -> 'a -> 'b list -> 'a * 'c list
-  val fold_right_map : ('b -> 'a -> 'c * 'a) -> 'b list -> 'a -> 'c list * 'a
-  val fold_left2_map : ('a -> 'b -> 'c -> 'a * 'd) -> 'a -> 'b list -> 'c list -> 'a * 'd list
-  val fold_right2_map : ('b -> 'c -> 'a -> 'd * 'a) -> 'b list -> 'c list -> 'a -> 'd list * 'a
-  val fold_left3_map : ('a -> 'b -> 'c -> 'd -> 'a * 'e) -> 'a -> 'b list -> 'c list -> 'd list -> 'a * 'e list
-  val fold_left4_map : ('a -> 'b -> 'c -> 'd -> 'e -> 'a * 'r) -> 'a -> 'b list -> 'c list -> 'd list -> 'e list -> 'a * 'r list
-  val fold_map : ('a -> 'b -> 'a * 'c) -> 'a -> 'b list -> 'a * 'c list
-  [@@ocaml.deprecated "Same as [fold_left_map]"]
-  val fold_map' : ('b -> 'a -> 'c * 'a) -> 'b list -> 'a -> 'c list * 'a
-  [@@ocaml.deprecated "Same as [fold_right_map]"]
   val map_assoc : ('a -> 'b) -> ('c * 'a) list -> ('c * 'b) list
   val assoc_f : 'a eq -> 'a -> ('a * 'b) list -> 'b
   val remove_assoc_f : 'a eq -> 'a -> ('a * 'b) list -> ('a * 'b) list
   val mem_assoc_f : 'a eq -> 'a -> ('a * 'b) list -> bool
+  val factorize_left : 'a eq -> ('a * 'b) list -> ('a * 'b list) list
+  val split : ('a * 'b) list -> 'a list * 'b list
+  val combine : 'a list -> 'b list -> ('a * 'b) list
+  val split3 : ('a * 'b * 'c) list -> 'a list * 'b list * 'c list
+  val combine3 : 'a list -> 'b list -> 'c list -> ('a * 'b * 'c) list
+  val add_set : 'a eq -> 'a -> 'a list -> 'a list
+  val eq_set : 'a eq -> 'a list -> 'a list -> bool
+  val subset : 'a list -> 'a list -> bool
+  val merge_set : 'a cmp -> 'a list -> 'a list -> 'a list
+  val intersect : 'a eq -> 'a list -> 'a list -> 'a list
+  val union : 'a eq -> 'a list -> 'a list -> 'a list
+  val unionq : 'a list -> 'a list -> 'a list
+  val subtract : 'a eq -> 'a list -> 'a list -> 'a list
+  val subtractq : 'a list -> 'a list -> 'a list
+  val merge_uniq : ('a -> 'a -> int) -> 'a list -> 'a list -> 'a list
+  val distinct : 'a list -> bool
+  val distinct_f : 'a cmp -> 'a list -> bool
+  val duplicates : 'a eq -> 'a list -> 'a list
+  val uniquize : 'a list -> 'a list
+  val sort_uniquize : 'a cmp -> 'a list -> 'a list
   val cartesian : ('a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list
   val cartesians : ('a -> 'b -> 'b) -> 'b -> 'a list list -> 'b list
   val combinations : 'a list list -> 'a list list
-  val combine3 : 'a list -> 'b list -> 'c list -> ('a * 'b * 'c) list
   val cartesians_filter :
     ('a -> 'b -> 'b option) -> 'b -> 'a list list -> 'b list
-  val factorize_left : 'a eq -> ('a * 'b) list -> ('a * 'b list) list
 
   module Smart :
   sig
     val map : ('a -> 'a) -> 'a list -> 'a list
-    val filter : ('a -> bool) -> 'a list -> 'a list
   end
 
   module type MonoS = sig
@@ -149,71 +156,71 @@ type 'a cell = {
 
 external cast : 'a cell -> 'a list = "%identity"
 
-let rec map_loop f p = function
-| [] -> ()
-| x :: l ->
-  let c = { head = f x; tail = [] } in
-  p.tail <- cast c;
-  map_loop f c l
+(** Extensions and redefinitions of OCaml Stdlib *)
 
-let map f = function
-| [] -> []
-| x :: l ->
-  let c = { head = f x; tail = [] } in
-  map_loop f c l;
-  cast c
+(** {6 Equality, testing} *)
 
-let rec map2_loop f p l1 l2 = match l1, l2 with
-| [], [] -> ()
-| x :: l1, y :: l2 ->
-  let c = { head = f x y; tail = [] } in
-  p.tail <- cast c;
-  map2_loop f c l1 l2
-| _ -> invalid_arg "List.map2"
+let rec compare cmp l1 l2 =
+  if l1 == l2 then 0 else
+  match l1,l2 with
+  | [], [] -> 0
+  | _::_, [] -> 1
+  | [], _::_ -> -1
+  | x1::l1, x2::l2 ->
+    match cmp x1 x2 with
+    | 0 -> compare cmp l1 l2
+    | c -> c
 
-let map2 f l1 l2 = match l1, l2 with
-| [], [] -> []
-| x :: l1, y :: l2 ->
-  let c = { head = f x y; tail = [] } in
-  map2_loop f c l1 l2;
-  cast c
-| _ -> invalid_arg "List.map2"
+let rec equal cmp l1 l2 =
+  l1 == l2 ||
+  match l1, l2 with
+  | [], [] -> true
+  | x1 :: l1, x2 :: l2 -> cmp x1 x2 && equal cmp l1 l2
+  | _ -> false
 
-let rec map_of_array_loop f p a i l =
-  if Int.equal i l then ()
-  else
-    let c = { head = f (Array.unsafe_get a i); tail = [] } in
-    p.tail <- cast c;
-    map_of_array_loop f c a (i + 1) l
+let is_empty = function
+  | [] -> true
+  | _ -> false
 
-let map_of_array f a =
-  let l = Array.length a in
-  if Int.equal l 0 then []
-  else
-    let c = { head = f (Array.unsafe_get a 0); tail = [] } in
-    map_of_array_loop f c a 1 l;
-    cast c
+let mem_f cmp x l =
+  List.exists (cmp x) l
 
-let rec append_loop p tl = function
-| [] -> p.tail <- tl
-| x :: l ->
-  let c = { head = x; tail = [] } in
-  p.tail <- cast c;
-  append_loop c tl l
+let for_all_i p =
+  let rec for_all_p i = function
+    | [] -> true
+    | a::l -> p i a && for_all_p (i+1) l
+  in
+  for_all_p
 
-let append l1 l2 = match l1 with
-| [] -> l2
-| x :: l ->
-  let c = { head = x; tail = [] } in
-  append_loop c l2 l;
-  cast c
+let for_all2eq f l1 l2 =
+  try List.for_all2 f l1 l2 with Invalid_argument _ -> false
 
-let rec copy p = function
-| [] -> p
-| x :: l ->
-  let c = { head = x; tail = [] } in
-  p.tail <- cast c;
-  copy c l
+let prefix_of cmp prefl l =
+  let rec prefrec = function
+    | (h1::t1, h2::t2) -> cmp h1 h2 && prefrec (t1,t2)
+    | ([], _) -> true
+    | _ -> false
+  in
+  prefrec (prefl,l)
+
+(** {6 Creating lists} *)
+
+let interval n m =
+  let rec interval_n (l,m) =
+    if n > m then l else interval_n (m::l, pred m)
+  in
+  interval_n ([], m)
+
+let addn n v =
+  let rec aux n l =
+    if Int.equal n 0 then l
+    else aux (pred n) (v :: l)
+  in
+  if n < 0 then invalid_arg "List.addn"
+  else aux n
+
+let make n v =
+  addn n v []
 
 let rec init_loop len f p i =
   if Int.equal i len then ()
@@ -230,9 +237,30 @@ let init len f =
     init_loop len f c 1;
     cast c
 
+let rec append_loop p tl = function
+  | [] -> p.tail <- tl
+  | x :: l ->
+    let c = { head = x; tail = [] } in
+    p.tail <- cast c;
+    append_loop c tl l
+
+let append l1 l2 = match l1 with
+  | [] -> l2
+  | x :: l ->
+    let c = { head = x; tail = [] } in
+    append_loop c l2 l;
+    cast c
+
+let rec copy p = function
+  | [] -> p
+  | x :: l ->
+    let c = { head = x; tail = [] } in
+    p.tail <- cast c;
+    copy c l
+
 let rec concat_loop p = function
-| [] -> ()
-| x :: l -> concat_loop (copy p x) l
+  | [] -> ()
+  | x :: l -> concat_loop (copy p x) l
 
 let concat l =
   let dummy = { head = Obj.magic 0; tail = [] } in
@@ -241,214 +269,272 @@ let concat l =
 
 let flatten = concat
 
-let rec split_loop p q = function
-| [] -> ()
-| (x, y) :: l ->
-  let cl = { head = x; tail = [] } in
-  let cr = { head = y; tail = [] } in
-  p.tail <- cast cl;
-  q.tail <- cast cr;
-  split_loop cl cr l
+(** {6 Lists as arrays} *)
 
-let split = function
-| [] -> [], []
-| (x, y) :: l ->
-  let cl = { head = x; tail = [] } in
-  let cr = { head = y; tail = [] } in
-  split_loop cl cr l;
-  (cast cl, cast cr)
-
-let rec combine_loop p l1 l2 = match l1, l2 with
-| [], [] -> ()
-| x :: l1, y :: l2 ->
-  let c = { head = (x, y); tail = [] } in
-  p.tail <- cast c;
-  combine_loop c l1 l2
-| _ -> invalid_arg "List.combine"
+let assign l n e =
+  let rec assrec stk l i = match l, i with
+    | (h :: t, 0) -> List.rev_append stk (e :: t)
+    | (h :: t, n) -> assrec (h :: stk) t (pred n)
+    | ([], _) -> failwith "List.assign"
+  in
+  assrec [] l n
 
-let combine l1 l2 = match l1, l2 with
-| [], [] -> []
-| x :: l1, y :: l2 ->
-  let c = { head = (x, y); tail = [] } in
-  combine_loop c l1 l2;
-  cast c
-| _ -> invalid_arg "List.combine"
+(** {6 Filtering} *)
 
 let rec filter_loop f p = function
-| [] -> ()
-| x :: l ->
-  if f x then
-    let c = { head = x; tail = [] } in
-    let () = p.tail <- cast c in
-    filter_loop f c l
-  else
-    filter_loop f p l
+  | [] -> ()
+  | x :: l' as l ->
+    let b = f x in
+    filter_loop f p l';
+    if b then if !p == l' then p := l else p := x :: !p
 
-let filter f l =
-  let c = { head = Obj.magic 0; tail = [] } in
-  filter_loop f c l;
-  c.tail
+let filter f = function
+  | [] -> []
+  | x :: l' as l ->
+    let p = ref [] in
+    let b = f x in
+    filter_loop f p l';
+    if b then if !p == l' then l else x :: !p else !p
 
-(** FIXME: Already present in OCaml 4.00 *)
+let rec filter2_loop f p q l1 l2 = match l1, l2 with
+  | [], [] -> ()
+  | x :: l1, y :: l2 ->
+    if f x y then
+      let c1 = { head = x; tail = [] } in
+      let c2 = { head = y; tail = [] } in
+      let () = p.tail <- cast c1 in
+      let () = q.tail <- cast c2 in
+      filter2_loop f c1 c2 l1 l2
+    else
+      filter2_loop f p q l1 l2
+  | _ -> invalid_arg "List.filter2"
 
-let rec map_i_loop f i p = function
-| [] -> ()
-| x :: l ->
-  let c = { head = f i x; tail = [] } in
-  p.tail <- cast c;
-  map_i_loop f (succ i) c l
+let filter2 f l1 l2 =
+  let c1 = { head = Obj.magic 0; tail = [] } in
+  let c2 = { head = Obj.magic 0; tail = [] } in
+  filter2_loop f c1 c2 l1 l2;
+  (c1.tail, c2.tail)
 
-let map_i f i = function
-| [] -> []
-| x :: l ->
-  let c = { head = f i x; tail = [] } in
-  map_i_loop f (succ i) c l;
-  cast c
+let filteri p =
+  let rec filter_i_rec i = function
+    | [] -> []
+    | x :: l -> let l' = filter_i_rec (succ i) l in if p i x then x :: l' else l'
+  in
+  filter_i_rec 0
 
-(** Extensions of OCaml Stdlib *)
+let smartfilter = filter (* Alias *)
 
-let rec compare cmp l1 l2 =
-  if l1 == l2 then 0 else
-  match l1,l2 with
-      [], [] -> 0
-    | _::_, [] -> 1
-    | [], _::_ -> -1
-    | x1::l1, x2::l2 ->
-        (match cmp x1 x2 with
-           | 0 -> compare cmp l1 l2
-           | c -> c)
+let rec filter_with filter l = match filter, l with
+  | [], [] -> []
+  | true :: filter, x :: l -> x :: filter_with filter l
+  | false :: filter, _ :: l -> filter_with filter l
+  | _ -> invalid_arg "List.filter_with"
 
-let rec equal cmp l1 l2 =
-  l1 == l2 ||
-  match l1, l2 with
-    | [], [] -> true
-    | x1 :: l1, x2 :: l2 ->
-      cmp x1 x2 && equal cmp l1 l2
-    | _ -> false
+let rec map_filter_loop f p = function
+  | [] -> ()
+  | x :: l ->
+    match f x with
+    | None -> map_filter_loop f p l
+    | Some y ->
+      let c = { head = y; tail = [] } in
+      p.tail <- cast c;
+      map_filter_loop f c l
 
-let is_empty = function
-| [] -> true
-| _ -> false
+let map_filter f l =
+  let c = { head = Obj.magic 0; tail = [] } in
+  map_filter_loop f c l;
+  c.tail
 
-let mem_f cmp x l = List.exists (cmp x) l
+let rec map_filter_i_loop f i p = function
+  | [] -> ()
+  | x :: l ->
+    match f i x with
+    | None -> map_filter_i_loop f (succ i) p l
+    | Some y ->
+      let c = { head = y; tail = [] } in
+      p.tail <- cast c;
+      map_filter_i_loop f (succ i) c l
 
-let intersect cmp l1 l2 =
-  filter (fun x -> mem_f cmp x l2) l1
+let map_filter_i f l =
+  let c = { head = Obj.magic 0; tail = [] } in
+  map_filter_i_loop f 0 c l;
+  c.tail
 
-let union cmp l1 l2 =
-  let rec urec = function
-    | [] -> l2
-    | a::l -> if mem_f cmp a l2 then urec l else a::urec l
+let partitioni p =
+  let rec aux i = function
+    | [] -> [], []
+    | x :: l ->
+      let (l1, l2) = aux (succ i) l in
+      if p i x then (x :: l1, l2)
+      else (l1, x :: l2)
   in
-  urec l1
+  aux 0
 
-let subtract cmp l1 l2 =
-  if is_empty l2 then l1
-  else List.filter (fun x -> not (mem_f cmp x l2)) l1
+(** {6 Applying functorially} *)
 
-let unionq l1 l2 = union (==) l1 l2
-let subtractq l1 l2 = subtract (==) l1 l2
+let rec map_loop f p = function
+  | [] -> ()
+  | x :: l ->
+    let c = { head = f x; tail = [] } in
+    p.tail <- cast c;
+    map_loop f c l
 
-let interval n m =
-  let rec interval_n (l,m) =
-    if n > m then l else interval_n (m::l, pred m)
-  in
-  interval_n ([], m)
+let map f = function
+  | [] -> []
+  | x :: l ->
+    let c = { head = f x; tail = [] } in
+    map_loop f c l;
+    cast c
 
-let addn n v =
-  let rec aux n l =
-    if Int.equal n 0 then l
-    else aux (pred n) (v :: l)
-  in
-  if n < 0 then invalid_arg "List.addn"
-  else aux n
+let rec map2_loop f p l1 l2 = match l1, l2 with
+  | [], [] -> ()
+  | x :: l1, y :: l2 ->
+    let c = { head = f x y; tail = [] } in
+    p.tail <- cast c;
+    map2_loop f c l1 l2
+  | _ -> invalid_arg "List.map2"
 
-let make n v = addn n v []
+let map2 f l1 l2 = match l1, l2 with
+  | [], [] -> []
+  | x :: l1, y :: l2 ->
+    let c = { head = f x y; tail = [] } in
+    map2_loop f c l1 l2;
+    cast c
+  | _ -> invalid_arg "List.map2"
 
-let assign l n e =
-  let rec assrec stk l i = match l, i with
-    | ((h::t), 0) -> List.rev_append stk (e :: t)
-    | ((h::t), n) -> assrec (h :: stk) t (pred n)
-    | ([], _) -> failwith "List.assign"
-  in
-  assrec [] l n
+(** Like OCaml [List.mapi] but tail-recursive *)
+
+let rec map_i_loop f i p = function
+  | [] -> ()
+  | x :: l ->
+    let c = { head = f i x; tail = [] } in
+    p.tail <- cast c;
+    map_i_loop f (succ i) c l
+
+let map_i f i = function
+  | [] -> []
+  | x :: l ->
+    let c = { head = f i x; tail = [] } in
+    map_i_loop f (succ i) c l;
+    cast c
 
 let map_left = map
 
 let map2_i f i l1 l2 =
   let rec map_i i = function
     | ([], []) -> []
-    | ((h1::t1), (h2::t2)) -> let v = f i h1 h2 in v :: map_i (succ i) (t1,t2)
+    | (h1 :: t1, h2 :: t2) -> let v = f i h1 h2 in v :: map_i (succ i) (t1,t2)
     | (_, _) -> invalid_arg "map2_i"
   in
   map_i i (l1,l2)
 
-let map3 f l1 l2 l3 =
-  let rec map = function
-    | ([], [], []) -> []
-    | ((h1::t1), (h2::t2), (h3::t3)) -> let v = f h1 h2 h3 in v::map (t1,t2,t3)
-    | (_, _, _) -> invalid_arg "map3"
-  in
-  map (l1,l2,l3)
+let rec map3_loop f p l1 l2 l3 = match l1, l2, l3 with
+  | [], [], [] -> ()
+  | x :: l1, y :: l2, z :: l3 ->
+    let c = { head = f x y z; tail = [] } in
+    p.tail <- cast c;
+    map3_loop f c l1 l2 l3
+  | _ -> invalid_arg "List.map3"
 
-let map4 f l1 l2 l3 l4 =
-  let rec map = function
-    | ([], [], [], []) -> []
-    | ((h1::t1), (h2::t2), (h3::t3), (h4::t4)) -> let v = f h1 h2 h3 h4 in v::map (t1,t2,t3,t4)
-    | (_, _, _, _) -> invalid_arg "map4"
-  in
-  map (l1,l2,l3,l4)
+let map3 f l1 l2 l3 = match l1, l2, l3 with
+  | [], [], [] -> []
+  | x :: l1, y :: l2, z :: l3 ->
+    let c = { head = f x y z; tail = [] } in
+    map3_loop f c l1 l2 l3;
+    cast c
+  | _ -> invalid_arg "List.map3"
+
+let rec map4_loop f p l1 l2 l3 l4 = match l1, l2, l3, l4 with
+  | [], [], [], [] -> ()
+  | x :: l1, y :: l2, z :: l3, t :: l4 ->
+    let c = { head = f x y z t; tail = [] } in
+    p.tail <- cast c;
+    map4_loop f c l1 l2 l3 l4
+  | _ -> invalid_arg "List.map4"
+
+let map4 f l1 l2 l3 l4 = match l1, l2, l3, l4 with
+  | [], [], [], [] -> []
+  | x :: l1, y :: l2, z :: l3, t :: l4 ->
+    let c = { head = f x y z t; tail = [] } in
+    map4_loop f c l1 l2 l3 l4;
+    cast c
+  | _ -> invalid_arg "List.map4"
+
+let rec map_of_array_loop f p a i l =
+  if Int.equal i l then ()
+  else
+    let c = { head = f (Array.unsafe_get a i); tail = [] } in
+    p.tail <- cast c;
+    map_of_array_loop f c a (i + 1) l
+
+let map_of_array f a =
+  let l = Array.length a in
+  if Int.equal l 0 then []
+  else
+    let c = { head = f (Array.unsafe_get a 0); tail = [] } in
+    map_of_array_loop f c a 1 l;
+    cast c
+
+let map_append f l = flatten (map f l)
+
+let map_append2 f l1 l2 = flatten (map2 f l1 l2)
 
 let rec extend l a l' = match l,l' with
-  | true::l, b::l' -> b :: extend l a l'
-  | false::l, l' -> a :: extend l a l'
+  | true :: l, b :: l' -> b :: extend l a l'
+  | false :: l, l' -> a :: extend l a l'
   | [], [] -> []
   | _ -> invalid_arg "extend"
 
 let count f l =
   let rec aux acc = function
     | [] -> acc
-    | h :: t -> if f h then aux (acc + 1) t else aux acc t in
+    | h :: t -> if f h then aux (acc + 1) t else aux acc t
+  in
   aux 0 l
 
+(** {6 Finding position} *)
+
 let rec index_f f x l n = match l with
-| [] -> raise Not_found
-| y :: l -> if f x y then n else index_f f x l (succ n)
+  | [] -> raise Not_found
+  | y :: l -> if f x y then n else index_f f x l (succ n)
 
 let index f x l = index_f f x l 1
 
 let index0 f x l = index_f f x l 0
 
+(** {6 Folding} *)
+
 let fold_left_until f accu s =
   let rec aux accu = function
     | [] -> accu
-    | x :: xs -> match f accu x with CSig.Stop x -> x | CSig.Cont i -> aux i xs in
+    | x :: xs -> match f accu x with CSig.Stop x -> x | CSig.Cont i -> aux i xs
+  in
   aux accu s
 
 let fold_right_i f i l =
   let rec it_f i l a = match l with
     | [] -> a
-    | b::l -> f (i-1) b (it_f (i-1) l a)
+    | b :: l -> f (i-1) b (it_f (i-1) l a)
   in
   it_f (List.length l + i) l
 
 let fold_left_i f =
   let rec it_list_f i a = function
     | [] -> a
-    | b::l -> it_list_f (i+1) (f i a b) l
+    | b :: l -> it_list_f (i+1) (f i a b) l
   in
   it_list_f
 
 let rec fold_left3 f accu l1 l2 l3 =
   match (l1, l2, l3) with
-    ([], [], []) -> accu
-  | (a1::l1, a2::l2, a3::l3) -> fold_left3 f (f accu a1 a2 a3) l1 l2 l3
+  | ([], [], []) -> accu
+  | (a1 :: l1, a2 :: l2, a3 :: l3) -> fold_left3 f (f accu a1 a2 a3) l1 l2 l3
   | (_, _, _) -> invalid_arg "List.fold_left3"
 
 let rec fold_left4 f accu l1 l2 l3 l4 =
   match (l1, l2, l3, l4) with
-    ([], [], [], []) -> accu
-  | (a1::l1, a2::l2, a3::l3, a4::l4) -> fold_left4 f (f accu a1 a2 a3 a4) l1 l2 l3 l4
+  | ([], [], [], []) -> accu
+  | (a1 :: l1, a2 :: l2, a3 :: l3, a4 :: l4) -> fold_left4 f (f accu a1 a2 a3 a4) l1 l2 l3 l4
   | (_,_, _, _) -> invalid_arg "List.fold_left4"
 
 (* [fold_right_and_left f [a1;...;an] hd =
@@ -466,214 +552,103 @@ let rec fold_left4 f accu l1 l2 l3 l4 =
 let fold_right_and_left f l hd =
   let rec aux tl = function
     | [] -> hd
-    | a::l -> let hd = aux (a::tl) l in f hd a tl
-   in aux [] l
+    | a :: l -> let hd = aux (a :: tl) l in f hd a tl
+  in
+  aux [] l
 
 (* Match sets as lists according to a matching function, also folding a side effect *)
 let rec fold_left2_set e f x l1 l2 =
   match l1 with
-  | a1::l1 ->
-     let rec find seen = function
-       | [] -> raise e
-       | a2::l2 ->
-          try fold_left2_set e f (f x a1 a2 l1 l2) l1 (List.rev_append seen l2)
-          with e' when e' = e -> find (a2::seen) l2 in
-     find [] l2
+  | a1 :: l1 ->
+      let rec find seen = function
+        | [] -> raise e
+        | a2 :: l2 ->
+            try fold_left2_set e f (f x a1 a2 l1 l2) l1 (List.rev_append seen l2)
+            with e' when e' = e -> find (a2 :: seen) l2 in
+      find [] l2
   | [] ->
-     if l2 = [] then x else raise e
+      if l2 = [] then x else raise e
+
+(* Poor man's monadic map *)
+let rec fold_left_map f e = function
+  | []  -> (e,[])
+  | h :: t ->
+    let e',h' = f e h in
+    let e'',t' = fold_left_map f e' t in
+    e'',h' :: t'
 
-let iteri f l = fold_left_i (fun i _ x -> f i x) 0 () l
+let fold_map = fold_left_map
 
-let for_all_i p =
-  let rec for_all_p i = function
-    | [] -> true
-    | a::l -> p i a && for_all_p (i+1) l
+(* (* tail-recursive version of the above function *)
+let fold_left_map f e l =
+  let g (e,b') h =
+    let (e',h') = f e h in
+      (e',h'::b')
   in
-  for_all_p
+  let (e',lrev) = List.fold_left g (e,[]) l in
+    (e',List.rev lrev)
+*)
+
+(* The same, based on fold_right, with the effect accumulated on the right *)
+let fold_right_map f l e =
+  List.fold_right (fun x (l,e) -> let (y,e) = f x e in (y::l,e)) l ([],e)
+
+let fold_map' = fold_right_map
+
+let on_snd f (x,y) = (x,f y)
+
+let fold_left2_map f e l l' =
+  on_snd List.rev @@
+  List.fold_left2 (fun (e,l) x x' ->
+      let (e,y) = f e x x' in
+      (e, y::l)
+    ) (e, []) l l'
+
+let fold_right2_map f l l' e =
+  List.fold_right2 (fun x x' (l,e) -> let (y,e) = f x x' e in (y::l,e)) l l' ([],e)
+
+let fold_left3_map f e l l' l'' =
+  on_snd List.rev @@
+  fold_left3 (fun (e,l) x x' x'' -> let (e,y) = f e x x' x'' in (e,y::l)) (e,[]) l l' l''
+
+let fold_left4_map f e l1 l2 l3 l4 =
+  on_snd List.rev @@
+  fold_left4 (fun (e,l) x1 x2 x3 x4 -> let (e,y) = f e x1 x2 x3 x4 in (e,y::l)) (e,[]) l1 l2 l3 l4
 
-let except cmp x l = List.filter (fun y -> not (cmp x y)) l
+(** {6 Splitting} *)
+
+let except cmp x l =
+  List.filter (fun y -> not (cmp x y)) l
 
 let remove = except (* Alias *)
 
 let rec remove_first p = function
-  | b::l when p b -> l
-  | b::l -> b::remove_first p l
+  | b :: l when p b -> l
+  | b :: l -> b :: remove_first p l
   | [] -> raise Not_found
 
 let extract_first p li =
   let rec loop rev_left = function
     | [] -> raise Not_found
-    | x::right ->
+    | x :: right ->
        if p x then List.rev_append rev_left right, x
        else loop (x :: rev_left) right
-  in loop [] li
+  in
+  loop [] li
 
 let insert p v l =
   let rec insrec = function
     | [] -> [v]
-    | h::tl -> if p v h then v::h::tl else h::insrec tl
+    | h :: tl -> if p v h then v :: h :: tl else h :: insrec tl
   in
   insrec l
 
-let add_set cmp x l = if mem_f cmp x l then l else x :: l
-
-(** List equality up to permutation (but considering multiple occurrences) *)
-
-let eq_set cmp l1 l2 =
-  let rec aux l1 = function
-  | [] -> is_empty l1
-  | a::l2 -> aux (remove_first (cmp a) l1) l2 in
-  try aux l1 l2 with Not_found -> false
-
-let for_all2eq f l1 l2 =
-  try List.for_all2 f l1 l2 with Invalid_argument _ -> false
-
-let filteri p =
-  let rec filter_i_rec i = function
-    | [] -> []
-    | x::l -> let l' = filter_i_rec (succ i) l in if p i x then x::l' else l'
-  in
-  filter_i_rec 0
-
-let partitioni p =
-  let rec aux i = function
-    | [] -> [], []
-    | x :: l ->
-        let (l1, l2) = aux (succ i) l in
-        if p i x then (x :: l1, l2)
-        else (l1, x :: l2)
-  in aux 0
-
-let rec sep_last = function
-  | [] -> failwith "sep_last"
-  | hd::[] -> (hd,[])
-  | hd::tl -> let (l,tl) = sep_last tl in (l,hd::tl)
-
 let rec find_map f = function
-| [] -> raise Not_found
-| x :: l ->
-  match f x with
-  | None -> find_map f l
-  | Some y -> y
-
-(* FIXME: we should avoid relying on the generic hash function,
-   just as we'd better avoid Pervasives.compare *)
-
-let uniquize l =
-  let visited = Hashtbl.create 23 in
-  let rec aux acc changed = function
-    | h::t -> if Hashtbl.mem visited h then aux acc true t else
-          begin
-            Hashtbl.add visited h h;
-            aux (h::acc) changed t
-          end
-    | [] -> if changed then List.rev acc else l
-  in aux [] false l
-
-(** [sort_uniquize] might be an alternative to the hashtbl-based
-    [uniquize], when the order of the elements is irrelevant *)
-
-let rec uniquize_sorted cmp = function
-  | a::b::l when Int.equal (cmp a b) 0 -> uniquize_sorted cmp (a::l)
-  | a::l -> a::uniquize_sorted cmp l
-  | [] -> []
-
-let sort_uniquize cmp l = uniquize_sorted cmp (List.sort cmp l)
-
-(* FIXME: again, generic hash function *)
-
-let distinct l =
-  let visited = Hashtbl.create 23 in
-  let rec loop = function
-    | h::t ->
-        if Hashtbl.mem visited h then false
-        else
-          begin
-            Hashtbl.add visited h h;
-            loop t
-          end
-    | [] -> true
-  in loop l
-
-let distinct_f cmp l =
-  let rec loop = function
-    | a::b::_ when Int.equal (cmp a b) 0 -> false
-    | a::l -> loop l
-    | [] -> true
-  in loop (List.sort cmp l)
-
-let rec merge_uniq cmp l1 l2 =
-  match l1, l2 with
-  | [], l2 -> l2
-  | l1, [] -> l1
-  | h1 :: t1, h2 :: t2 ->
-      let c = cmp h1 h2 in
-      if Int.equal c 0
-      then h1 :: merge_uniq cmp t1 t2
-      else if c <= 0
-      then h1 :: merge_uniq cmp t1 l2
-      else h2 :: merge_uniq cmp l1 t2
-
-let rec duplicates cmp = function
-  | [] -> []
-  | x::l ->
-      let l' = duplicates cmp l in
-      if mem_f cmp x l then add_set cmp x l' else l'
-
-let rec filter2_loop f p q l1 l2 = match l1, l2 with
-| [], [] -> ()
-| x :: l1, y :: l2 ->
-  if f x y then
-    let c1 = { head = x; tail = [] } in
-    let c2 = { head = y; tail = [] } in
-    let () = p.tail <- cast c1 in
-    let () = q.tail <- cast c2 in
-    filter2_loop f c1 c2 l1 l2
-  else
-    filter2_loop f p q l1 l2
-| _ -> invalid_arg "List.filter2"
-
-let filter2 f l1 l2 =
-  let c1 = { head = Obj.magic 0; tail = [] } in
-  let c2 = { head = Obj.magic 0; tail = [] } in
-  filter2_loop f c1 c2 l1 l2;
-  (c1.tail, c2.tail)
-
-let rec map_filter_loop f p = function
-  | [] -> ()
+  | [] -> raise Not_found
   | x :: l ->
     match f x with
-    | None -> map_filter_loop f p l
-    | Some y ->
-      let c = { head = y; tail = [] } in
-      p.tail <- cast c;
-      map_filter_loop f c l
-
-let map_filter f l =
-  let c = { head = Obj.magic 0; tail = [] } in
-  map_filter_loop f c l;
-  c.tail
-
-let rec map_filter_i_loop f i p = function
-  | [] -> ()
-  | x :: l ->
-    match f i x with
-    | None -> map_filter_i_loop f (succ i) p l
-    | Some y ->
-      let c = { head = y; tail = [] } in
-      p.tail <- cast c;
-      map_filter_i_loop f (succ i) c l
-
-let map_filter_i f l =
-  let c = { head = Obj.magic 0; tail = [] } in
-  map_filter_i_loop f 0 c l;
-  c.tail
-
-let rec filter_with filter l = match filter, l with
-| [], [] -> []
-| true :: filter, x :: l -> x :: filter_with filter l
-| false :: filter, _ :: l -> filter_with filter l
-| _ -> invalid_arg "List.filter_with"
+    | None -> find_map f l
+    | Some y -> y
 
 (* FIXME: again, generic hash function *)
 
@@ -682,7 +657,7 @@ let subset l1 l2 =
   List.iter (fun x -> Hashtbl.add t2 x ()) l2;
   let rec look = function
     | [] -> true
-    | x::ll -> try Hashtbl.find t2 x; look ll with Not_found -> false
+    | x :: ll -> try Hashtbl.find t2 x; look ll with Not_found -> false
   in
   look l1
 
@@ -694,7 +669,7 @@ exception IndexOutOfRange
 let goto n l =
   let rec goto i acc = function
     | tl when Int.equal i 0 -> (acc, tl)
-    | h::t -> goto (pred i) (h::acc) t
+    | h :: t -> goto (pred i) (h :: acc) t
     | [] -> raise IndexOutOfRange
   in
   goto n [] l
@@ -715,29 +690,36 @@ let chop n l =
 let split_when p =
   let rec split_when_loop x y =
     match y with
-      | []      -> (List.rev x,[])
-      | (a::l)  -> if (p a) then (List.rev x,y) else split_when_loop (a::x) l
+    | [] -> (List.rev x,[])
+    | (a :: l)  -> if (p a) then (List.rev x,y) else split_when_loop (a :: x) l
   in
   split_when_loop []
 
-let rec split3 = function
-  | [] -> ([], [], [])
-  | (x,y,z)::l ->
-      let (rx, ry, rz) = split3 l in (x::rx, y::ry, z::rz)
-
 let firstn n l =
   let rec aux acc n l =
     match n, l with
     | 0, _ -> List.rev acc
-    | n, h::t -> aux (h::acc) (pred n) t
+    | n, h :: t -> aux (h :: acc) (pred n) t
     | _ -> failwith "firstn"
   in
   aux [] n l
 
+let rec sep_last = function
+  | [] -> failwith "sep_last"
+  | hd :: [] -> (hd,[])
+  | hd :: tl -> let (l,tl) = sep_last tl in (l,hd :: tl)
+
+(* Drop the last element of a list *)
+
+let rec drop_last = function
+  | [] -> failwith "drop_last"
+  | hd :: [] -> []
+  | hd :: tl -> hd :: drop_last tl
+
 let rec last = function
   | [] -> failwith "List.last"
-  | [x] -> x
-  | _ :: l -> last l
+  | hd :: [] -> hd
+  | _ :: tl -> last tl
 
 let lastn n l =
   let len = List.length l in
@@ -749,96 +731,216 @@ let lastn n l =
 let rec skipn n l = match n,l with
   | 0, _ -> l
   | _, [] -> failwith "List.skipn"
-  | n, _::l -> skipn (pred n) l
+  | n, _ :: l -> skipn (pred n) l
 
 let skipn_at_least n l =
-  try skipn n l with Failure _ -> []
-
-let prefix_of cmp prefl l =
-  let rec prefrec = function
-    | (h1::t1, h2::t2) -> cmp h1 h2 && prefrec (t1,t2)
-    | ([], _) -> true
-    | _ -> false
-  in
-  prefrec (prefl,l)
+  try skipn n l with Failure _ when n >= 0 -> []
 
 (** if [l=p++t] then [drop_prefix p l] is [t] else [l] *)
 
 let drop_prefix cmp p l =
   let rec drop_prefix_rec = function
-    | (h1::tp, h2::tl) when cmp h1 h2 -> drop_prefix_rec (tp,tl)
+    | (h1 :: tp, h2 :: tl) when cmp h1 h2 -> drop_prefix_rec (tp,tl)
     | ([], tl) -> tl
     | _ -> l
   in
   drop_prefix_rec (p,l)
 
-let map_append f l = List.flatten (List.map f l)
-
-let map_append2 f l1 l2 = List.flatten (List.map2 f l1 l2)
-
 let share_tails l1 l2 =
   let rec shr_rev acc = function
-    | ((x1::l1), (x2::l2)) when x1 == x2 -> shr_rev (x1::acc) (l1,l2)
-    | (l1,l2) -> (List.rev l1, List.rev l2, acc)
+    | (x1 :: l1, x2 :: l2) when x1 == x2 -> shr_rev (x1 :: acc) (l1,l2)
+    | (l1, l2) -> (List.rev l1, List.rev l2, acc)
   in
   shr_rev [] (List.rev l1, List.rev l2)
 
-(* Poor man's monadic map *)
-let rec fold_left_map f e = function
-  | []  -> (e,[])
-  | h::t ->
-    let e',h' = f e h in
-    let e'',t' = fold_left_map f e' t in
-    e'',h'::t'
+(** {6 Association lists} *)
 
-let fold_map = fold_left_map
+let map_assoc f = List.map (fun (x,a) -> (x,f a))
 
-(* (* tail-recursive version of the above function *)
-let fold_map f e l =
-  let g (e,b') h =
-    let (e',h') = f e h in
-      (e',h'::b')
+let rec assoc_f f a = function
+  | (x, e) :: xs -> if f a x then e else assoc_f f a xs
+  | [] -> raise Not_found
+
+let remove_assoc_f f a l =
+  try remove_first (fun (x,_) -> f a x) l with Not_found -> l
+
+let mem_assoc_f f a l = List.exists (fun (x,_) -> f a x) l
+
+(** {6 Operations on lists of tuples} *)
+
+let rec split_loop p q = function
+  | [] -> ()
+  | (x, y) :: l ->
+    let cl = { head = x; tail = [] } in
+    let cr = { head = y; tail = [] } in
+    p.tail <- cast cl;
+    q.tail <- cast cr;
+    split_loop cl cr l
+
+let split = function
+  | [] -> [], []
+  | (x, y) :: l ->
+    let cl = { head = x; tail = [] } in
+    let cr = { head = y; tail = [] } in
+    split_loop cl cr l;
+    (cast cl, cast cr)
+
+let rec combine_loop p l1 l2 = match l1, l2 with
+  | [], [] -> ()
+  | x :: l1, y :: l2 ->
+    let c = { head = (x, y); tail = [] } in
+    p.tail <- cast c;
+    combine_loop c l1 l2
+  | _ -> invalid_arg "List.combine"
+
+let combine l1 l2 = match l1, l2 with
+  | [], [] -> []
+  | x :: l1, y :: l2 ->
+    let c = { head = (x, y); tail = [] } in
+    combine_loop c l1 l2;
+    cast c
+  | _ -> invalid_arg "List.combine"
+
+let rec split3_loop p q r = function
+  | [] -> ()
+  | (x, y, z) :: l ->
+    let cp = { head = x; tail = [] } in
+    let cq = { head = y; tail = [] } in
+    let cr = { head = z; tail = [] } in
+    p.tail <- cast cp;
+    q.tail <- cast cq;
+    r.tail <- cast cr;
+    split3_loop cp cq cr l
+
+let split3 = function
+  | [] -> [], [], []
+  | (x, y, z) :: l ->
+    let cp = { head = x; tail = [] } in
+    let cq = { head = y; tail = [] } in
+    let cr = { head = z; tail = [] } in
+    split3_loop cp cq cr l;
+    (cast cp, cast cq, cast cr)
+
+let rec combine3_loop p l1 l2 l3 = match l1, l2, l3 with
+  | [], [], [] -> ()
+  | x :: l1, y :: l2, z :: l3 ->
+    let c = { head = (x, y, z); tail = [] } in
+    p.tail <- cast c;
+    combine3_loop c l1 l2 l3
+  | _ -> invalid_arg "List.combine3"
+
+let combine3 l1 l2 l3 = match l1, l2, l3 with
+  | [], [], [] -> []
+  | x :: l1, y :: l2, z :: l3 ->
+    let c = { head = (x, y, z); tail = [] } in
+    combine3_loop c l1 l2 l3;
+    cast c
+  | _ -> invalid_arg "List.combine3"
+
+(** {6 Operations on lists seen as sets, preserving uniqueness of elements} *)
+
+(** Add an element, preserving uniqueness of elements *)
+
+let add_set cmp x l =
+  if mem_f cmp x l then l else x :: l
+
+(** List equality up to permutation (but considering multiple occurrences) *)
+
+let eq_set cmp l1 l2 =
+  let rec aux l1 = function
+  | [] -> is_empty l1
+  | a :: l2 -> aux (remove_first (cmp a) l1) l2
   in
-  let (e',lrev) = List.fold_left g (e,[]) l in
-    (e',List.rev lrev)
-*)
+  try aux l1 l2 with Not_found -> false
 
-(* The same, based on fold_right, with the effect accumulated on the right *)
-let fold_right_map f l e =
-  List.fold_right (fun x (l,e) -> let (y,e) = f x e in (y::l,e)) l ([],e)
+let rec merge_set cmp l1 l2 = match l1, l2 with
+  | [], l2 -> l2
+  | l1, [] -> l1
+  | h1 :: t1, h2 :: t2 ->
+    let c = cmp h1 h2 in
+    if Int.equal c 0
+    then h1 :: merge_set cmp t1 t2
+    else if c <= 0
+    then h1 :: merge_set cmp t1 l2
+    else h2 :: merge_set cmp l1 t2
 
-let fold_map' = fold_right_map
+let merge_uniq = merge_set
 
-let on_snd f (x,y) = (x,f y)
+let intersect cmp l1 l2 =
+  filter (fun x -> mem_f cmp x l2) l1
 
-let fold_left2_map f e l l' =
-  on_snd List.rev @@
-  List.fold_left2 (fun (e,l) x x' ->
-      let (e,y) = f e x x' in
-      (e, y::l)
-    ) (e, []) l l'
+let union cmp l1 l2 =
+  let rec urec = function
+    | [] -> l2
+    | a :: l -> if mem_f cmp a l2 then urec l else a :: urec l
+  in
+  urec l1
 
-let fold_right2_map f l l' e =
-  List.fold_right2 (fun x x' (l,e) -> let (y,e) = f x x' e in (y::l,e)) l l' ([],e)
+let subtract cmp l1 l2 =
+  if is_empty l2 then l1
+  else List.filter (fun x -> not (mem_f cmp x l2)) l1
 
-let fold_left3_map f e l l' l'' =
-  on_snd List.rev @@
-  fold_left3 (fun (e,l) x x' x'' -> let (e,y) = f e x x' x'' in (e,y::l)) (e,[]) l l' l''
+let unionq l1 l2 = union (==) l1 l2
+let subtractq l1 l2 = subtract (==) l1 l2
 
-let fold_left4_map f e l1 l2 l3 l4 =
-  on_snd List.rev @@
-  fold_left4 (fun (e,l) x1 x2 x3 x4 -> let (e,y) = f e x1 x2 x3 x4 in (e,y::l)) (e,[]) l1 l2 l3 l4
+(** {6 Uniqueness and duplication} *)
 
-let map_assoc f = List.map (fun (x,a) -> (x,f a))
+(* FIXME: we should avoid relying on the generic hash function,
+   just as we'd better avoid Pervasives.compare *)
 
-let rec assoc_f f a = function
-  | (x, e) :: xs -> if f a x then e else assoc_f f a xs
-  | [] -> raise Not_found
+let distinct l =
+  let visited = Hashtbl.create 23 in
+  let rec loop = function
+    | h :: t ->
+        if Hashtbl.mem visited h then false
+        else
+          begin
+            Hashtbl.add visited h h;
+            loop t
+          end
+    | [] -> true
+  in
+  loop l
 
-let remove_assoc_f f a l =
-  try remove_first (fun (x,_) -> f a x) l with Not_found -> l
+let distinct_f cmp l =
+  let rec loop = function
+    | a :: b :: _ when Int.equal (cmp a b) 0 -> false
+    | a :: l -> loop l
+    | [] -> true
+  in loop (List.sort cmp l)
 
-let mem_assoc_f f a l = List.exists (fun (x,_) -> f a x) l
+(* FIXME: again, generic hash function *)
+
+let uniquize l =
+  let visited = Hashtbl.create 23 in
+  let rec aux acc changed = function
+    | h :: t -> if Hashtbl.mem visited h then aux acc true t else
+          begin
+            Hashtbl.add visited h h;
+            aux (h :: acc) changed t
+          end
+    | [] -> if changed then List.rev acc else l
+  in
+  aux [] false l
+
+(** [sort_uniquize] might be an alternative to the hashtbl-based
+    [uniquize], when the order of the elements is irrelevant *)
+
+let rec uniquize_sorted cmp = function
+  | a :: b :: l when Int.equal (cmp a b) 0 -> uniquize_sorted cmp (a :: l)
+  | a :: l -> a :: uniquize_sorted cmp l
+  | [] -> []
+
+let sort_uniquize cmp l =
+  uniquize_sorted cmp (List.sort cmp l)
+
+let rec duplicates cmp = function
+  | [] -> []
+  | x :: l ->
+      let l' = duplicates cmp l in
+      if mem_f cmp x l then add_set cmp x l' else l'
+
+(** {6 Cartesian product} *)
 
 (* A generic cartesian product: for any operator (**),
    [cartesian (**) [x1;x2] [y1;y2] = [x1**y1; x1**y2; x2**y1; x2**y1]],
@@ -855,15 +957,9 @@ let cartesians op init ll =
 
 (* combinations [[a;b];[c;d]] gives [[a;c];[a;d];[b;c];[b;d]] *)
 
-let combinations l = cartesians (fun x l -> x::l) [] l
+let combinations l =
+  cartesians (fun x l -> x :: l) [] l
 
-let rec combine3 x y z = 
-  match x, y, z with
-  | [], [], [] -> []
-  | (x :: xs), (y :: ys), (z :: zs) ->
-      (x, y, z) :: combine3 xs ys zs
-  | _, _, _ -> invalid_arg "List.combine3"
-  
 (* Keep only those products that do not return None *)
 
 let cartesian_filter op l1 l2 =
@@ -874,43 +970,34 @@ let cartesian_filter op l1 l2 =
 let cartesians_filter op init ll =
   List.fold_right (cartesian_filter op) ll [init]
 
-(* Drop the last element of a list *)
-
-let rec drop_last = function
-  | [] -> assert false
-  | hd :: [] -> []
-  | hd :: tl -> hd :: drop_last tl
-
 (* Factorize lists of pairs according to the left argument *)
 let rec factorize_left cmp = function
-  | (a,b)::l ->
+  | (a,b) :: l ->
       let al,l' = partition (fun (a',_) -> cmp a a') l in
-      (a,(b::List.map snd al)) :: factorize_left cmp l'
+      (a,(b :: List.map snd al)) :: factorize_left cmp l'
   | [] -> []
 
 module Smart =
 struct
 
-  let rec map f l = match l with
-    [] -> l
-  | h::tl ->
-      let h' = f h and tl' = map f tl in
-        if h'==h && tl'==tl then l
-        else h'::tl'
-
-  let rec filter f l = match l with
-    [] -> l
-  | h::tl ->
-      let tl' = filter f tl in
-        if f h then
-          if tl' == tl then l
-          else h :: tl'
-        else tl'
+  let rec map_loop f p = function
+    | [] -> ()
+    | x :: l' as l ->
+      let x' = f x in
+      map_loop f p l';
+      if x' == x && !p == l' then p := l else p := x' :: !p
+
+  let map f = function
+    | [] -> []
+    | x :: l' as l ->
+      let p = ref [] in
+      let x' = f x in
+      map_loop f p l';
+      if x' == x && !p == l' then l else x' :: !p
 
 end
 
 let smartmap = Smart.map
-let smartfilter = Smart.filter
 
 module type MonoS = sig
   type elt
diff --git a/clib/cList.mli b/clib/cList.mli
index b3c151098..d080ebca2 100644
--- a/clib/cList.mli
+++ b/clib/cList.mli
@@ -18,33 +18,31 @@ module type ExtS =
 sig
   include S
 
+  (** {6 Equality, testing} *)
+
   val compare : 'a cmp -> 'a list cmp
   (** Lexicographic order on lists. *)
 
   val equal : 'a eq -> 'a list eq
-  (** Lifts equality to list type. *)
+  (** Lift equality to list type. *)
 
   val is_empty : 'a list -> bool
-  (** Checks whether a list is empty *)
-
-  val init : int -> (int -> 'a) -> 'a list
-  (** [init n f] constructs the list [f 0; ... ; f (n - 1)]. *)
+  (** Check whether a list is empty *)
 
   val mem_f : 'a eq -> 'a -> 'a list -> bool
-  (* Same as [List.mem], for some specific equality *)
+  (** Same as [List.mem], for some specific equality *)
 
-  val add_set : 'a eq -> 'a -> 'a list -> 'a list
-  (** [add_set x l] adds [x] in [l] if it is not already there, or returns [l]
-      otherwise. *)
+  val for_all_i : (int -> 'a -> bool) -> int -> 'a list -> bool
+  (** Same as [List.for_all] but with an index *)
 
-  val eq_set : 'a eq -> 'a list eq
-  (** Test equality up to permutation (but considering multiple occurrences) *)
+  val for_all2eq : ('a -> 'b -> bool) -> 'a list -> 'b list -> bool
+  (** Same as [List.for_all2] but returning [false] when of different length *)
 
-  val intersect : 'a eq -> 'a list -> 'a list -> 'a list
-  val union : 'a eq -> 'a list -> 'a list -> 'a list
-  val unionq : 'a list -> 'a list -> 'a list
-  val subtract : 'a eq -> 'a list -> 'a list -> 'a list
-  val subtractq : 'a list -> 'a list -> 'a list
+  val prefix_of : 'a eq -> 'a list eq
+  (** [prefix_of eq l1 l2] returns [true] if [l1] is a prefix of [l2], [false]
+      otherwise. It uses [eq] to compare elements *)
+
+  (** {6 Creating lists} *)
 
   val interval : int -> int -> int list
   (** [interval i j] creates the list [[i; i + 1; ...; j]], or [[]] when 
@@ -52,27 +50,66 @@ sig
 
   val make : int -> 'a -> 'a list
   (** [make n x] returns a list made of [n] times [x]. Raise
-      [Invalid_argument "List.make"] if [n] is negative. *)
+      [Invalid_argument _] if [n] is negative. *)
 
-  val assign : 'a list -> int -> 'a -> 'a list
-  (** [assign l i x] sets the [i]-th element of [l] to [x], starting from [0]. *)
+  val addn : int -> 'a -> 'a list -> 'a list
+  (** [addn n x l] adds [n] times [x] on the left of [l]. *)
 
-  val distinct : 'a list -> bool
-  (** Return [true] if all elements of the list are distinct. *)
+  val init : int -> (int -> 'a) -> 'a list
+  (** [init n f] constructs the list [f 0; ... ; f (n - 1)]. Raise
+      [Invalid_argument _] if [n] is negative *)
 
-  val distinct_f : 'a cmp -> 'a list -> bool
+  val append : 'a list -> 'a list -> 'a list
+  (** Like OCaml's [List.append] but tail-recursive. *)
 
-  val duplicates : 'a eq -> 'a list -> 'a list
-  (** Return the list of unique elements which appear at least twice. Elements
-      are kept in the order of their first appearance. *)
+  val concat : 'a list list -> 'a list
+  (** Like OCaml's [List.concat] but tail-recursive. *)
+
+  val flatten : 'a list list -> 'a list
+  (** Synonymous of [concat] *)
+
+  (** {6 Lists as arrays} *)
+
+  val assign : 'a list -> int -> 'a -> 'a list
+  (** [assign l i x] sets the [i]-th element of [l] to [x], starting
+      from [0]. Raise [Failure _] if [i] is out of range. *)
+
+  (** {6 Filtering} *)
+
+  val filter : ('a -> bool) -> 'a list -> 'a list
+  (** Like OCaml [List.filter] but tail-recursive and physically returns
+      the original list if the predicate holds for all elements. *)
 
   val filter2 : ('a -> 'b -> bool) -> 'a list -> 'b list -> 'a list * 'b list
+  (** Like [List.filter] but with 2 arguments, raise [Invalid_argument _]
+      if the lists are not of same length. *)
+
+  val filteri : (int -> 'a -> bool) -> 'a list -> 'a list
+  (** Like [List.filter] but with an index starting from [0] *)
+
+  val filter_with : bool list -> 'a list -> 'a list
+  (** [filter_with bl l] selects elements of [l] whose corresponding element in
+      [bl] is [true]. Raise [Invalid_argument _] if sizes differ. *)
+
+  val smartfilter : ('a -> bool) -> 'a list -> 'a list
+  [@@ocaml.deprecated "Same as [filter]"]
+
   val map_filter : ('a -> 'b option) -> 'a list -> 'b list
+  (** Like [map] but keeping only non-[None] elements *)
+
   val map_filter_i : (int -> 'a -> 'b option) -> 'a list -> 'b list
+  (** Like [map_filter] but with an index starting from [0] *)
 
-  val filter_with : bool list -> 'a list -> 'a list
-  (** [filter_with b a] selects elements of [a] whose corresponding element in
-      [b] is [true]. Raise [Invalid_argument _] when sizes differ. *)
+  val partitioni : (int -> 'a -> bool) -> 'a list -> 'a list * 'a list
+  (** Like [List.partition] but with an index starting from [0] *)
+
+  (** {6 Applying functorially} *)
+
+  val map : ('a -> 'b) -> 'a list -> 'b list
+  (** Like OCaml [List.map] but tail-recursive *)
+
+  val map2 : ('a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list
+  (** Like OCaml [List.map2] but tail-recursive *)
 
   val smartmap : ('a -> 'a) -> 'a list -> 'a list
   [@@ocaml.deprecated "Same as [Smart.map]"]
@@ -81,27 +118,39 @@ sig
   (** As [map] but ensures the left-to-right order of evaluation. *)
 
   val map_i : (int -> 'a -> 'b) -> int -> 'a list -> 'b list
-  (** As [map] but with the index, which starts from [0]. *)
+  (** Like OCaml [List.mapi] but tail-recursive. Alternatively, like
+      [map] but with an index *)
 
   val map2_i :
     (int -> 'a -> 'b -> 'c) -> int -> 'a list -> 'b list -> 'c list
+  (** Like [map2] but with an index *)
+
   val map3 :
     ('a -> 'b -> 'c -> 'd) -> 'a list -> 'b list -> 'c list -> 'd list
+  (** Like [map] but for 3 lists. *)
+
   val map4 : ('a -> 'b -> 'c -> 'd -> 'e) -> 'a list -> 'b list -> 'c list ->
     'd list -> 'e list
-  val filteri : (int -> 'a -> bool) -> 'a list -> 'a list
-  val partitioni : (int -> 'a -> bool) -> 'a list -> 'a list * 'a list
+  (** Like [map] but for 4 lists. *)
 
   val map_of_array : ('a -> 'b) -> 'a array -> 'b list
   (** [map_of_array f a] behaves as [List.map f (Array.to_list a)] *)
 
-  val smartfilter : ('a -> bool) -> 'a list -> 'a list
-  [@@ocaml.deprecated "Same as [Smart.filter]"]
+  val map_append : ('a -> 'b list) -> 'a list -> 'b list
+  (** [map_append f [x1; ...; xn]] returns [f x1 @ ... @ f xn]. *)
+
+  val map_append2 : ('a -> 'b -> 'c list) -> 'a list -> 'b list -> 'c list
+  (** Like [map_append] but for two lists; raises [Invalid_argument _]
+      if the two lists do not have the same length. *)
 
   val extend : bool list -> 'a -> 'a list -> 'a list
-(** [extend l a [a1..an]] assumes that the number of [true] in [l] is [n];
+  (** [extend l a [a1..an]] assumes that the number of [true] in [l] is [n];
     it extends [a1..an] by inserting [a] at the position of [false] in [l] *)
+
   val count : ('a -> bool) -> 'a list -> int
+  (** Count the number of elements satisfying a predicate *)
+
+  (** {6 Finding position} *)
 
   val index : 'a eq -> 'a -> 'a list -> int
   (** [index] returns the 1st index of an element in a list (counting from 1). *)
@@ -109,29 +158,65 @@ sig
   val index0 : 'a eq -> 'a -> 'a list -> int
   (** [index0] behaves as [index] except that it starts counting at 0. *)
 
-  val iteri :  (int -> 'a -> unit) -> 'a list -> unit
-  (** As [iter] but with the index argument (starting from 0). *)
+  (** {6 Folding} *)
 
   val fold_left_until : ('c -> 'a -> 'c CSig.until) -> 'c -> 'a list -> 'c
   (** acts like [fold_left f acc s] while [f] returns
       [Cont acc']; it stops returning [c] as soon as [f] returns [Stop c]. *)
 
   val fold_right_i :  (int -> 'a -> 'b -> 'b) -> int -> 'a list -> 'b -> 'b
+  (** Like [List.fold_right] but with an index *)
+
   val fold_left_i :  (int -> 'a -> 'b -> 'a) -> int -> 'a -> 'b list -> 'a
-  val fold_right_and_left :
-      ('a -> 'b -> 'b list -> 'a) -> 'b list -> 'a -> 'a
+  (** Like [List.fold_left] but with an index *)
+
+  val fold_right_and_left : ('b -> 'a -> 'a list -> 'b) -> 'a list -> 'b -> 'b
+  (** [fold_right_and_left f [a1;...;an] hd] is
+      [f (f (... (f (f hd an [an-1;...;a1]) an-1 [an-2;...;a1]) ...) a2 [a1]) a1 []] *)
+
   val fold_left3 : ('a -> 'b -> 'c -> 'd -> 'a) -> 'a -> 'b list -> 'c list -> 'd list -> 'a
+  (** Like [List.fold_left] but for 3 lists; raise [Invalid_argument _] if
+      not all lists of the same size *)
 
+  val fold_left2_set : exn -> ('a -> 'b -> 'c -> 'b list -> 'c list -> 'a) -> 'a -> 'b list -> 'c list -> 'a
   (** Fold sets, i.e. lists up to order; the folding function tells
       when elements match by returning a value and raising the given
       exception otherwise; sets should have the same size; raise the
       given exception if no pairing of the two sets is found;;
       complexity in O(n^2) *)
-  val fold_left2_set : exn -> ('a -> 'b -> 'c -> 'b list -> 'c list -> 'a) -> 'a -> 'b list -> 'c list -> 'a
 
-  val for_all_i : (int -> 'a -> bool) -> int -> 'a list -> bool
+  val fold_left_map : ('a -> 'b -> 'a * 'c) -> 'a -> 'b list -> 'a * 'c list
+  (** [fold_left_map f e_0 [a1;...;an]] is [e_n,[k_1...k_n]]
+      where [(e_i,k_i)] is [f e_{i-1} ai] for each i<=n *)
+
+  val fold_right_map : ('b -> 'a -> 'c * 'a) -> 'b list -> 'a -> 'c list * 'a
+  (** Same, folding on the right *)
+
+  val fold_left2_map : ('a -> 'b -> 'c -> 'a * 'd) -> 'a -> 'b list -> 'c list -> 'a * 'd list
+  (** Same with two lists, folding on the left *)
+
+  val fold_right2_map : ('b -> 'c -> 'a -> 'd * 'a) -> 'b list -> 'c list -> 'a -> 'd list * 'a
+  (** Same with two lists, folding on the right *)
+
+  val fold_left3_map : ('a -> 'b -> 'c -> 'd -> 'a * 'e) -> 'a -> 'b list -> 'c list -> 'd list -> 'a * 'e list
+  (** Same with three lists, folding on the left *)
+
+  val fold_left4_map : ('a -> 'b -> 'c -> 'd -> 'e -> 'a * 'r) -> 'a -> 'b list -> 'c list -> 'd list -> 'e list -> 'a * 'r list
+  (** Same with four lists, folding on the left *)
+
+  val fold_map : ('a -> 'b -> 'a * 'c) -> 'a -> 'b list -> 'a * 'c list
+  [@@ocaml.deprecated "Same as [fold_left_map]"]
+
+  val fold_map' : ('b -> 'a -> 'c * 'a) -> 'b list -> 'a -> 'c list * 'a
+  [@@ocaml.deprecated "Same as [fold_right_map]"]
+
+  (** {6 Splitting} *)
+
   val except : 'a eq -> 'a -> 'a list -> 'a list
+  (** [except eq a l] Remove all occurrences of [a] in [l] *)
+
   val remove : 'a eq -> 'a -> 'a list -> 'a list
+  (** Alias of [except] *)
 
   val remove_first : ('a -> bool) -> 'a list -> 'a list
   (** Remove the first element satisfying a predicate, or raise [Not_found] *)
@@ -140,35 +225,10 @@ sig
   (** Remove and return the first element satisfying a predicate,
       or raise [Not_found] *)
 
-  val insert : ('a -> 'a -> bool) -> 'a -> 'a list -> 'a list
-  (** Insert at the (first) position so that if the list is ordered wrt to the
-      total order given as argument, the order is preserved *)
-
-  val for_all2eq : ('a -> 'b -> bool) -> 'a list -> 'b list -> bool
-  val sep_last : 'a list -> 'a * 'a list
-
   val find_map : ('a -> 'b option) -> 'a list -> 'b
   (** Returns the first element that is mapped to [Some _]. Raise [Not_found] if
       there is none. *)
 
-  val uniquize : 'a list -> 'a list
-  (** Return the list of elements without duplicates.
-      This is the list unchanged if there was none. *)
-
-  val sort_uniquize : 'a cmp -> 'a list -> 'a list
-  (** Return a sorted and de-duplicated version of a list,
-      according to some comparison function. *)
-
-  val merge_uniq : 'a cmp -> 'a list -> 'a list -> 'a list
-  (** Merge two sorted lists and preserves the uniqueness property. *)
-
-  val subset : 'a list -> 'a list -> bool
-
-  val chop : int -> 'a list -> 'a list * 'a list
-  (** [chop i l] splits [l] into two lists [(l1,l2)] such that
-      [l1++l2=l] and [l1] has length [i].  It raises [Failure] when [i]
-      is negative or greater than the length of [l] *)
-
   exception IndexOutOfRange
   val goto: int -> 'a list -> 'a list * 'a list
   (** [goto i l] splits [l] into two lists [(l1,l2)] such that
@@ -176,95 +236,174 @@ sig
       [IndexOutOfRange] when [i] is negative or greater than the
       length of [l]. *)
 
-
   val split_when : ('a -> bool) -> 'a list -> 'a list * 'a list
-  val split3 : ('a * 'b * 'c) list -> 'a list * 'b list * 'c list
-  val firstn : int -> 'a list -> 'a list
+  (** [split_when p l] splits [l] into two lists [(l1,a::l2)] such that
+      [l1++(a::l2)=l], [p a=true] and [p b = false] for every element [b] of [l1].
+      if there is no such [a], then it returns [(l,[])] instead. *)
+
+  val sep_last : 'a list -> 'a * 'a list
+  (** [sep_last l] returns [(a,l')] such that [l] is [l'@[a]].
+      It raises [Failure _] if the list is empty. *)
+
+  val drop_last : 'a list -> 'a list
+  (** Remove the last element of the list. It raises [Failure _] if the
+      list is empty. This is the second part of [sep_last]. *)
+
   val last : 'a list -> 'a
+  (** Return the last element of the list. It raises [Failure _] if the
+      list is empty. This is the first part of [sep_last]. *)
+
   val lastn : int -> 'a list -> 'a list
+  (** [lastn n l] returns the [n] last elements of [l]. It raises
+      [Failure _] if [n] is less than 0 or larger than the length of [l] *)
+
+  val chop : int -> 'a list -> 'a list * 'a list
+  (** [chop i l] splits [l] into two lists [(l1,l2)] such that
+      [l1++l2=l] and [l1] has length [i]. It raises [Failure _] when
+      [i] is negative or greater than the length of [l]. *)
+
+  val firstn : int -> 'a list -> 'a list
+  (** [firstn n l] Returns the [n] first elements of [l]. It raises
+      [Failure _] if [n] negative or too large. This is the first part
+      of [chop]. *)
+
   val skipn : int -> 'a list -> 'a list
+  (** [skipn n l] drops the [n] first elements of [l]. It raises
+      [Failure _] if [n] is less than 0 or larger than the length of [l].
+      This is the second part of [chop]. *)
+
   val skipn_at_least : int -> 'a list -> 'a list
+  (** Same as [skipn] but returns [] if [n] is larger than the list of
+      the list. *)
 
-  val addn : int -> 'a -> 'a list -> 'a list
-  (** [addn n x l] adds [n] times [x] on the left of [l]. *)
+  val drop_prefix : 'a eq -> 'a list -> 'a list -> 'a list
+  (** [drop_prefix eq l1 l] returns [l2] if [l=l1++l2] else return [l]. *)
+
+  val insert : 'a eq -> 'a -> 'a list -> 'a list
+  (** Insert at the (first) position so that if the list is ordered wrt to the
+      total order given as argument, the order is preserved *)
+
+  val share_tails : 'a list -> 'a list -> 'a list * 'a list * 'a list
+  (** [share_tails l1 l2] returns [(l1',l2',l)] such that [l1] is
+      [l1'@l] and [l2] is [l2'@l] and [l] is maximal amongst all such
+      decompositions*)
+
+  (** {6 Association lists} *)
+
+  val map_assoc : ('a -> 'b) -> ('c * 'a) list -> ('c * 'b) list
+  (** Applies a function on the codomain of an association list *)
+
+  val assoc_f : 'a eq -> 'a -> ('a * 'b) list -> 'b
+  (** Like [List.assoc] but using the equality given as argument *)
+
+  val remove_assoc_f : 'a eq -> 'a -> ('a * 'b) list -> ('a * 'b) list
+  (** Remove first matching element; unchanged if no such element *)
+
+  val mem_assoc_f : 'a eq -> 'a -> ('a * 'b) list -> bool
+  (** Like [List.mem_assoc] but using the equality given as argument *)
 
-  val prefix_of : 'a eq -> 'a list -> 'a list -> bool
-  (** [prefix_of l1 l2] returns [true] if [l1] is a prefix of [l2], [false]
+  val factorize_left : 'a eq -> ('a * 'b) list -> ('a * 'b list) list
+  (** Create a list of associations from a list of pairs *)
+
+  (** {6 Operations on lists of tuples} *)
+
+  val split : ('a * 'b) list -> 'a list * 'b list
+  (** Like OCaml's [List.split] but tail-recursive. *)
+
+  val combine : 'a list -> 'b list -> ('a * 'b) list
+  (** Like OCaml's [List.combine] but tail-recursive. *)
+
+  val split3 : ('a * 'b * 'c) list -> 'a list * 'b list * 'c list
+  (** Like [split] but for triples *)
+
+  val combine3 : 'a list -> 'b list -> 'c list -> ('a * 'b * 'c) list
+  (** Like [combine] but for triples *)
+
+  (** {6 Operations on lists seen as sets, preserving uniqueness of elements} *)
+
+  val add_set : 'a eq -> 'a -> 'a list -> 'a list
+  (** [add_set x l] adds [x] in [l] if it is not already there, or returns [l]
       otherwise. *)
 
-  val drop_prefix : 'a eq -> 'a list -> 'a list -> 'a list
-  (** [drop_prefix p l] returns [t] if [l=p++t] else return [l]. *)
+  val eq_set : 'a eq -> 'a list eq
+  (** Test equality up to permutation. It respects multiple occurrences
+      and thus works also on multisets. *)
 
-  val drop_last : 'a list -> 'a list
+  val subset : 'a list eq
+  (** Tell if a list is a subset of another up to permutation. It expects
+      each element to occur only once. *)
 
-  val map_append : ('a -> 'b list) -> 'a list -> 'b list
-  (** [map_append f [x1; ...; xn]] returns [(f x1)@(f x2)@...@(f xn)]. *)
+  val merge_set : 'a cmp -> 'a list -> 'a list -> 'a list
+  (** Merge two sorted lists and preserves the uniqueness property. *)
 
-  val map_append2 : ('a -> 'b -> 'c list) -> 'a list -> 'b list -> 'c list
-  (** As [map_append]. Raises [Invalid_argument _] if the two lists don't have 
-      the same length. *)
+  val intersect : 'a eq -> 'a list -> 'a list -> 'a list
+  (** Return the intersection of two lists, assuming and preserving
+      uniqueness of elements *)
 
-  val share_tails : 'a list -> 'a list -> 'a list * 'a list * 'a list
+  val union : 'a eq -> 'a list -> 'a list -> 'a list
+  (** Return the union of two lists, assuming and preserving
+      uniqueness of elements *)
 
-  val fold_left_map : ('a -> 'b -> 'a * 'c) -> 'a -> 'b list -> 'a * 'c list
-  (** [fold_left_map f e_0 [l_1...l_n] = e_n,[k_1...k_n]]
-    where [(e_i,k_i)=f e_{i-1} l_i] *)
+  val unionq : 'a list -> 'a list -> 'a list
+  (** [union] specialized to physical equality *)
 
-  val fold_right_map : ('b -> 'a -> 'c * 'a) -> 'b list -> 'a -> 'c list * 'a
-  (** Same, folding on the right *)
+  val subtract : 'a eq -> 'a list -> 'a list -> 'a list
+  (** Remove from the first list all elements from the second list. *)
 
-  val fold_left2_map : ('a -> 'b -> 'c -> 'a * 'd) -> 'a -> 'b list -> 'c list -> 'a * 'd list
-  (** Same with two lists, folding on the left *)
+  val subtractq : 'a list -> 'a list -> 'a list
+  (** [subtract] specialized to physical equality *)
 
-  val fold_right2_map : ('b -> 'c -> 'a -> 'd * 'a) -> 'b list -> 'c list -> 'a -> 'd list * 'a
-  (** Same with two lists, folding on the right *)
+  val merge_uniq : 'a cmp -> 'a list -> 'a list -> 'a list
+  (** [@@ocaml.deprecated "Same as [merge_set]"] *)
 
-  val fold_left3_map : ('a -> 'b -> 'c -> 'd -> 'a * 'e) -> 'a -> 'b list -> 'c list -> 'd list -> 'a * 'e list
-  (** Same with three lists, folding on the left *)
+  (** {6 Uniqueness and duplication} *)
 
-  val fold_left4_map : ('a -> 'b -> 'c -> 'd -> 'e -> 'a * 'r) -> 'a -> 'b list -> 'c list -> 'd list -> 'e list -> 'a * 'r list
-  (** Same with four lists, folding on the left *)
+  val distinct : 'a list -> bool
+  (** Return [true] if all elements of the list are distinct. *)
 
-  val fold_map : ('a -> 'b -> 'a * 'c) -> 'a -> 'b list -> 'a * 'c list
-  [@@ocaml.deprecated "Same as [fold_left_map]"]
+  val distinct_f : 'a cmp -> 'a list -> bool
+  (** Like [distinct] but using the equality given as argument *)
 
-  val fold_map' : ('b -> 'a -> 'c * 'a) -> 'b list -> 'a -> 'c list * 'a
-  [@@ocaml.deprecated "Same as [fold_right_map]"]
+  val duplicates : 'a eq -> 'a list -> 'a list
+  (** Return the list of unique elements which appear at least twice. Elements
+      are kept in the order of their first appearance. *)
 
-  val map_assoc : ('a -> 'b) -> ('c * 'a) list -> ('c * 'b) list
-  val assoc_f : 'a eq -> 'a -> ('a * 'b) list -> 'b
-  val remove_assoc_f : 'a eq -> 'a -> ('a * 'b) list -> ('a * 'b) list
-  val mem_assoc_f : 'a eq -> 'a -> ('a * 'b) list -> bool
+  val uniquize : 'a list -> 'a list
+  (** Return the list of elements without duplicates.
+      This is the list unchanged if there was none. *)
+
+  val sort_uniquize : 'a cmp -> 'a list -> 'a list
+  (** Return a sorted version of a list without duplicates
+      according to some comparison function. *)
+
+  (** {6 Cartesian product} *)
 
   val cartesian : ('a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list
-  (** A generic cartesian product: for any operator (**),
+  (** A generic binary cartesian product: for any operator (**),
     [cartesian (**) [x1;x2] [y1;y2] = [x1**y1; x1**y2; x2**y1; x2**y1]],
     and so on if there are more elements in the lists. *)
 
   val cartesians : ('a -> 'b -> 'b) -> 'b -> 'a list list -> 'b list
-  (** [cartesians] is an n-ary cartesian product: it iterates
-    [cartesian] over a list of lists.  *)
+  (** [cartesians op init l] is an n-ary cartesian product: it builds
+      the list of all [op a1 .. (op an init) ..] for [a1], ..., [an] in
+      the product of the elements of the lists *)
 
   val combinations : 'a list list -> 'a list list
-  (** combinations [[a;b];[c;d]] returns [[a;c];[a;d];[b;c];[b;d]] *)
-
-  val combine3 : 'a list -> 'b list -> 'c list -> ('a * 'b * 'c) list
+  (** [combinations l] returns the list of [n_1] * ... * [n_p] tuples
+      [[a11;...;ap1];...;[a1n_1;...;apn_pd]] whenever [l] is a list
+      [[a11;..;a1n_1];...;[ap1;apn_p]]; otherwise said, it is
+      [cartesians (::) [] l] *)
 
   val cartesians_filter :
     ('a -> 'b -> 'b option) -> 'b -> 'a list list -> 'b list
-  (** Keep only those products that do not return None *)
-
-  val factorize_left : 'a eq -> ('a * 'b) list -> ('a * 'b list) list
+  (** Like [cartesians op init l] but keep only the tuples for which
+      [op] returns [Some _] on all the elements of the tuple. *)
 
   module Smart :
   sig
     val map : ('a -> 'a) -> 'a list -> 'a list
     (** [Smart.map f [a1...an] = List.map f [a1...an]] but if for all i
         [f ai == ai], then [Smart.map f l == l] *)
-
-    val filter : ('a -> bool) -> 'a list -> 'a list
-    (** [Smart.filter f [a1...an] = List.filter f [a1...an]] but if for all i
-        [f ai = true], then [Smart.filter f l == l] *)
   end
 
   module type MonoS = sig