Moving Utils.list_* to a proper CList module, which includes stdlib

List module. That way, an "open Util" in the header permits using
any function of CList in the List namespace (and in particular, this
permits optimized reimplementations of the List functions, as, for
example, tail-rec implementations.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15801 85f007b7-540e-0410-9357-904b9bb8a0f7

6 files changed, 913 insertions, 661 deletions

diff --git a/lib/cList.ml b/lib/cList.ml
new file mode 100644
index 0000000000..e3f35dcacb
--- /dev/null
+++ b/lib/cList.ml
@@ -0,0 +1,718 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+
+module type S =
+sig
+  val length : 'a list -> int
+  val hd : 'a list -> 'a
+  val tl : 'a list -> 'a list
+  val nth : 'a list -> int -> 'a
+  val rev : 'a list -> 'a list
+  val append : 'a list -> 'a list -> 'a list
+  val rev_append : 'a list -> 'a list -> 'a list
+  val concat : 'a list list -> 'a list
+  val flatten : 'a list list -> 'a list
+  val iter : ('a -> unit) -> 'a list -> unit
+  val map : ('a -> 'b) -> 'a list -> 'b list
+  val rev_map : ('a -> 'b) -> 'a list -> 'b list
+  val fold_left : ('a -> 'b -> 'a) -> 'a -> 'b list -> 'a
+  val fold_right : ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b
+  val iter2 : ('a -> 'b -> unit) -> 'a list -> 'b list -> unit
+  val map2 : ('a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list
+  val rev_map2 : ('a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list
+  val fold_left2 : ('a -> 'b -> 'c -> 'a) -> 'a -> 'b list -> 'c list -> 'a
+  val fold_right2 : ('a -> 'b -> 'c -> 'c) -> 'a list -> 'b list -> 'c -> 'c
+  val for_all : ('a -> bool) -> 'a list -> bool
+  val exists : ('a -> bool) -> 'a list -> bool
+  val for_all2 : ('a -> 'b -> bool) -> 'a list -> 'b list -> bool
+  val exists2 : ('a -> 'b -> bool) -> 'a list -> 'b list -> bool
+  val mem : 'a -> 'a list -> bool
+  val memq : 'a -> 'a list -> bool
+  val find : ('a -> bool) -> 'a list -> 'a
+  val filter : ('a -> bool) -> 'a list -> 'a list
+  val find_all : ('a -> bool) -> 'a list -> 'a list
+  val partition : ('a -> bool) -> 'a list -> 'a list * 'a list
+  val assoc : 'a -> ('a * 'b) list -> 'b
+  val assq : 'a -> ('a * 'b) list -> 'b
+  val mem_assoc : 'a -> ('a * 'b) list -> bool
+  val mem_assq : 'a -> ('a * 'b) list -> bool
+  val remove_assoc : 'a -> ('a * 'b) list -> ('a * 'b) list
+  val remove_assq : 'a -> ('a * 'b) list -> ('a * 'b) list
+  val split : ('a * 'b) list -> 'a list * 'b list
+  val combine : 'a list -> 'b list -> ('a * 'b) list
+  val sort : ('a -> 'a -> int) -> 'a list -> 'a list
+  val stable_sort : ('a -> 'a -> int) -> 'a list -> 'a list
+  val fast_sort : ('a -> 'a -> int) -> 'a list -> 'a list
+  val merge : ('a -> 'a -> int) -> 'a list -> 'a list -> 'a list
+end
+
+module type ExtS =
+sig
+  include S
+  val compare : ('a -> 'a -> int) -> 'a list -> 'a list -> int
+  val equal : ('a -> 'a -> bool) -> 'a list -> 'a list -> bool
+  val add_set : 'a -> 'a list -> 'a list
+  val eq_set : 'a list -> 'a list -> bool
+  val intersect : 'a list -> 'a list -> 'a list
+  val union : 'a list -> 'a list -> 'a list
+  val unionq : 'a list -> 'a list -> 'a list
+  val subtract : 'a list -> 'a list -> 'a list
+  val subtractq : 'a list -> 'a list -> 'a list
+
+  (** [tabulate f n] builds [[f 0; ...; f (n-1)]] *)
+  val tabulate : (int -> 'a) -> int -> 'a list
+  val make : int -> 'a -> 'a list
+  val assign : 'a list -> int -> 'a -> 'a list
+  val distinct : 'a list -> bool
+  val duplicates : 'a list -> 'a list
+  val filter2 : ('a -> 'b -> bool) -> 'a list * 'b list -> 'a list * 'b list
+  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 filter_along : ('a -> bool) -> 'a list -> 'b list -> 'b list
+
+  (** [smartmap f [a1...an] = List.map f [a1...an]] but if for all i
+    [ f ai == ai], then [smartmap f l==l] *)
+  val smartmap : ('a -> 'a) -> 'a list -> 'a list
+  val map_left : ('a -> 'b) -> 'a list -> 'b list
+  val map_i : (int -> 'a -> 'b) -> int -> 'a list -> 'b list
+  val map2_i :
+    (int -> 'a -> 'b -> 'c) -> int -> 'a list -> 'b list -> 'c list
+  val map3 :
+    ('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 map_to_array : ('a -> 'b) -> 'a list -> 'b array
+  val filter_i :
+    (int -> 'a -> bool) -> 'a list -> 'a list
+
+  (** [smartfilter f [a1...an] = List.filter f [a1...an]] but if for all i
+    [f ai = true], then [smartfilter f l==l] *)
+  val smartfilter : ('a -> bool) -> 'a list -> 'a list
+
+  (** [index] returns the 1st index of an element in a list (counting from 1) *)
+  val index : 'a -> 'a list -> int
+  val index_f : ('a -> 'a -> bool) -> 'a -> 'a list -> int
+
+  (** [unique_index x l] returns [Not_found] if [x] doesn't occur exactly once *)
+  val unique_index : 'a -> 'a list -> int
+
+  (** [index0] behaves as [index] except that it starts counting at 0 *)
+  val index0 : 'a -> 'a list -> int
+  val index0_f : ('a -> 'a -> bool) -> 'a -> 'a list -> int
+  val iter3 : ('a -> 'b -> 'c -> unit) -> 'a list -> 'b list -> 'c list -> unit
+  val iter_i :  (int -> 'a -> unit) -> 'a list -> unit
+  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
+  val fold_right_and_left :
+      ('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 for_all_i : (int -> 'a -> bool) -> int -> 'a list -> bool
+  val except : 'a -> 'a list -> 'a list
+  val remove : 'a -> 'a list -> 'a list
+  val remove_first : 'a -> 'a list -> 'a list
+  val remove_assoc_in_triple : 'a -> ('a * 'b * 'c) list -> ('a * 'b * 'c) list
+  val assoc_snd_in_triple : 'a -> ('a * 'b * 'c) list -> 'b
+  val for_all2eq : ('a -> 'b -> bool) -> 'a list -> 'b list -> bool
+  val sep_last : 'a list -> 'a * 'a list
+  val try_find_i : (int -> 'a -> 'b) -> int -> 'a list -> 'b
+  val try_find : ('a -> 'b) -> 'a list -> 'b
+  val uniquize : 'a list -> 'a list
+
+  (** merges two sorted lists and preserves the uniqueness property: *)
+  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
+  (* former [split_at] was a duplicate of [chop] *)
+  val split_when : ('a -> bool) -> 'a list -> 'a list * 'a list
+  val split_by : ('a -> bool) -> 'a list -> 'a list * 'a list
+  val split3 : ('a * 'b * 'c) list -> 'a list * 'b list * 'c list
+  val partition_by : ('a -> 'a -> bool) -> 'a list -> 'a list list
+  val firstn : int -> 'a list -> 'a list
+  val last : 'a list -> 'a
+  val lastn : 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 list -> 'a list -> bool
+
+  (** [drop_prefix p l] returns [t] if [l=p++t] else return [l] *)
+  val drop_prefix : 'a list -> 'a list -> 'a list
+  val drop_last : 'a list -> 'a list
+
+  (** [map_append f [x1; ...; xn]] returns [(f x1)@(f x2)@...@(f xn)] *)
+  val map_append : ('a -> 'b list) -> 'a list -> 'b list
+  val join_map : ('a -> 'b list) -> 'a list -> 'b list
+
+  (** raises [Invalid_argument] if the two lists don't have the same length *)
+  val map_append2 : ('a -> 'b -> 'c list) -> 'a list -> 'b list -> 'c list
+  val share_tails : 'a list -> 'a list -> 'a list * 'a list * 'a list
+
+  (** [fold_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 fold_map : ('a -> 'b -> 'a * 'c) -> 'a -> 'b list -> 'a * 'c list
+  val fold_map' : ('b -> 'a -> 'c * 'a) -> 'b list -> 'a -> 'c list * 'a
+  val map_assoc : ('a -> 'b) -> ('c * 'a) list -> ('c * 'b) list
+  val assoc_f : ('a -> 'a -> bool) -> 'a -> ('a * 'b) list -> 'b
+
+  (** A generic 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 cartesian : ('a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list
+
+  (** [cartesians] is an n-ary cartesian product: it iterates
+    [cartesian] over a list of lists.  *)
+  val cartesians : ('a -> 'b -> 'b) -> 'b -> 'a list list -> 'b list
+
+  (** combinations [[a;b];[c;d]] returns [[a;c];[a;d];[b;c];[b;d]] *)
+  val combinations : 'a list list -> 'a list list
+  val combine3 : 'a list -> 'b list -> 'c list -> ('a * 'b * 'c) list
+
+  (** Keep only those products that do not return None *)
+  val cartesian_filter :
+    ('a -> 'b -> 'c option) -> 'a list -> 'b list -> 'c list
+  val cartesians_filter :
+    ('a -> 'b -> 'b option) -> 'b -> 'a list list -> 'b list
+
+  val union_map : ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b
+  val factorize_left : ('a * 'b) list -> ('a * 'b list) list
+end
+
+include List
+
+(* Lists *)
+
+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 equal cmp l1 l2 =
+  l1 == l2 ||
+  match l1, l2 with
+    | [], [] -> true
+    | x1 :: l1, x2 :: l2 ->
+      cmp x1 x2 && equal cmp l1 l2
+    | _ -> false
+
+let intersect l1 l2 =
+  List.filter (fun x -> List.mem x l2) l1
+
+let union l1 l2 =
+  let rec urec = function
+    | [] -> l2
+    | a::l -> if List.mem a l2 then urec l else a::urec l
+  in
+  urec l1
+
+let unionq l1 l2 =
+  let rec urec = function
+    | [] -> l2
+    | a::l -> if List.memq a l2 then urec l else a::urec l
+  in
+  urec l1
+
+let subtract l1 l2 =
+  if l2 = [] then l1 else List.filter (fun x -> not (List.mem x l2)) l1
+
+let subtractq l1 l2 =
+  if l2 = [] then l1 else List.filter (fun x -> not (List.memq x l2)) l1
+
+let tabulate f len =
+  let rec tabrec n =
+    if n = len then [] else (f n)::(tabrec (n+1))
+  in
+  tabrec 0
+
+let addn n v =
+  let rec aux n l =
+    if 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 assign l n e =
+  let rec assrec stk = function
+    | ((h::t), 0) -> List.rev_append stk (e::t)
+    | ((h::t), n) -> assrec (h::stk) (t, n-1)
+    | ([], _) -> failwith "List.assign"
+  in
+  assrec [] (l,n)
+
+let rec smartmap f l = match l with
+    [] -> l
+  | h::tl ->
+      let h' = f h and tl' = smartmap f tl in
+        if h'==h && tl'==tl then l
+        else h'::tl'
+
+let map_left f = (* ensures the order in case of side-effects *)
+  let rec map_rec = function
+    | [] -> []
+    | x::l -> let v = f x in v :: map_rec l
+  in
+  map_rec
+
+let map_i f =
+  let rec map_i_rec i = function
+    | [] -> []
+    | x::l -> let v = f i x in v :: map_i_rec (i+1) l
+  in
+  map_i_rec
+
+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)
+    | (_, _) -> 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 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 map_to_array f l =
+  Array.of_list (List.map f l)
+
+let rec smartfilter f l = match l with
+    [] -> l
+  | h::tl ->
+      let tl' = smartfilter f tl in
+        if f h then
+          if tl' == tl then l
+          else h :: tl'
+        else tl'
+          
+let index_f f x =
+  let rec index_x n = function
+    | y::l -> if f x y then n else index_x (succ n) l
+    | [] -> raise Not_found
+  in
+  index_x 1
+
+let index0_f f x l = index_f f x l - 1
+
+let index x =
+  let rec index_x n = function
+    | y::l -> if x = y then n else index_x (succ n) l
+    | [] -> raise Not_found
+  in
+  index_x 1
+
+let index0 x l = index x l - 1
+
+let unique_index x =
+  let rec index_x n = function
+    | y::l ->
+        if x = y then
+          if List.mem x l then raise Not_found
+          else n
+        else index_x (succ n) l
+    | [] -> raise Not_found
+  in index_x 1
+
+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)
+  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
+  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
+  | (_, _, _) -> invalid_arg "List.fold_left3"
+
+(* [fold_right_and_left f [a1;...;an] hd =
+   f (f (... (f (f hd
+                   an
+                   [an-1;...;a1])
+              an-1
+              [an-2;...;a1])
+         ...)
+        a2
+        [a1])
+     a1
+     []] *)
+
+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
+
+let iter3 f l1 l2 l3 =
+  let rec iter = function
+    | ([], [], []) -> ()
+    | ((h1::t1), (h2::t2), (h3::t3)) -> f h1 h2 h3; iter (t1,t2,t3)
+    | (_, _, _) -> invalid_arg "map3"
+  in
+  iter (l1,l2,l3)
+
+let iter_i f l = fold_left_i (fun i _ x -> f i x) 0 () 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 except x l = List.filter (fun y -> not (x = y)) l
+
+let remove = except (* Alias *)
+
+let rec remove_first a = function
+  | b::l when a = b -> l
+  | b::l -> b::remove_first a l
+  | [] -> raise Not_found
+
+let rec remove_assoc_in_triple x = function
+  | [] -> []
+  | (y,_,_ as z)::l -> if x = y then l else z::remove_assoc_in_triple x l
+
+let rec assoc_snd_in_triple x = function
+    [] -> raise Not_found
+  | (a,b,_)::l -> if Pervasives.compare a x = 0 then b else assoc_snd_in_triple x l
+
+let add_set x l = if List.mem x l then l else x::l
+
+let eq_set l1 l2 =
+  let rec aux l1 = function
+  | [] -> l1 = []
+  | a::l2 -> aux (remove_first 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 filter_i 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 rec sep_last = function
+  | [] -> failwith "sep_last"
+  | hd::[] -> (hd,[])
+  | hd::tl -> let (l,tl) = sep_last tl in (l,hd::tl)
+
+let try_find_i f =
+  let rec try_find_f n = function
+    | [] -> failwith "try_find_i"
+    | h::t -> try f n h with Failure _ -> try_find_f (n+1) t
+  in
+  try_find_f
+
+let try_find f =
+  let rec try_find_f = function
+    | [] -> failwith "try_find"
+    | h::t -> try f h with Failure _ -> try_find_f t
+  in
+  try_find_f
+
+let uniquize l =
+  let visited = Hashtbl.create 23 in
+  let rec aux acc = function
+    | h::t -> if Hashtbl.mem visited h then aux acc t else
+          begin
+            Hashtbl.add visited h h;
+            aux (h::acc) t
+          end
+    | [] -> List.rev acc
+  in aux [] l
+
+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 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 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 = function
+  | [] -> []
+  | x::l ->
+      let l' = duplicates l in
+      if List.mem x l then add_set x l' else l'
+
+let rec filter2 f = function
+  | [], [] as p -> p
+  | d::dp, l::lp ->
+     let (dp',lp' as p) = filter2 f (dp,lp) in
+      if f d l then d::dp', l::lp' else p
+  | _ -> invalid_arg "List.filter2"
+
+let rec map_filter f = function
+  | [] -> []
+  | x::l ->
+      let l' = map_filter f l in
+      match f x with None -> l' | Some y -> y::l'
+
+let map_filter_i f =
+  let rec aux i = function
+    | [] -> []
+    | x::l ->
+      let l' = aux (succ i) l in
+        match f i x with None -> l' | Some y -> y::l'
+  in aux 0
+
+let filter_along f filter l =
+  snd (filter2 (fun b c -> f b) (filter,l))
+
+let filter_with filter l =
+  filter_along (fun x -> x) filter l
+
+let subset l1 l2 =
+  let t2 = Hashtbl.create 151 in
+  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
+  in
+  look l1
+
+(* [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]  *)
+
+let chop n l =
+  let rec chop_aux i acc = function
+    | tl when i=0 -> (List.rev acc, tl)
+    | h::t -> chop_aux (pred i) (h::acc) t
+    | [] -> failwith "List.chop"
+  in
+  chop_aux n [] l
+
+(* [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 *)
+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
+  in
+  split_when_loop []
+
+(* [split_by p l] splits [l] into two lists [(l1,l2)] such that elements of
+   [l1] satisfy [p] and elements of [l2] do not; order is preserved *)
+let split_by p =
+  let rec split_by_loop = function
+  | []   -> ([],[])
+  | a::l ->
+      let (l1,l2) = split_by_loop l in if p a then (a::l1,l2) else (l1,a::l2)
+  in
+  split_by_loop
+
+let rec split3 = function
+  | [] -> ([], [], [])
+  | (x,y,z)::l ->
+      let (rx, ry, rz) = split3 l in (x::rx, y::ry, z::rz)
+
+let rec insert_in_class f a = function
+  | [] -> [[a]]
+  | (b::_ as l)::classes when f a b -> (a::l)::classes
+  | l::classes -> l :: insert_in_class f a classes
+
+let partition_by f l =
+  List.fold_right (insert_in_class f) l []
+
+let firstn n l =
+  let rec aux acc = function
+    | (0, l) -> List.rev acc
+    | (n, (h::t)) -> aux (h::acc) (pred n, t)
+    | _ -> failwith "firstn"
+  in
+  aux [] (n,l)
+
+let rec last = function
+  | [] -> failwith "List.last"
+  | [x] -> x
+  | _ :: l -> last l
+
+let lastn n l =
+  let len = List.length l in
+  let rec aux m l =
+    if m = n then l else aux (m - 1) (List.tl l)
+  in
+  if len < n then failwith "lastn" else aux len l
+
+let rec skipn n l = match n,l with
+  | 0, _ -> l
+  | _, [] -> failwith "List.skipn"
+  | n, _::l -> skipn (pred n) l
+
+let skipn_at_least n l =
+  try skipn n l with Failure _ -> []
+
+let prefix_of prefl l =
+  let rec prefrec = function
+    | (h1::t1, h2::t2) -> h1 = h2 && prefrec (t1,t2)
+    | ([], _) -> true
+    | (_, _) -> false
+  in
+    prefrec (prefl,l)
+
+let drop_prefix p l =
+(* if l=p++t then return t else l *)
+  let rec drop_prefix_rec = function
+    | ([], tl) -> Some tl
+    | (_, []) -> None
+    | (h1::tp, h2::tl) ->
+        if h1 = h2 then drop_prefix_rec (tp,tl) else None
+  in
+    match drop_prefix_rec (p,l) with
+      | Some r -> r
+      | None -> l
+
+let map_append f l = List.flatten (List.map f l)
+let join_map = map_append   (* Alias *)
+
+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)
+  in
+  shr_rev [] (List.rev l1, List.rev l2)
+
+let rec fold_map f e = function
+  |  []  -> (e,[])
+  |  h::t ->
+       let e',h' = f e h in
+       let e'',t' = fold_map f e' t in
+         e'',h'::t'
+
+(* (* 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')
+  in
+  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_map' f l e =
+  List.fold_right (fun x (l,e) -> let (y,e) = f x e in (y::l,e)) l ([],e)
+
+let map_assoc f = List.map (fun (x,a) -> (x,f a))
+
+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
+
+(* Specification:
+   - =p= is set equality (double inclusion)
+   - f such that \forall l acc, (f l acc) =p= append (f l []) acc
+   - let g = fun x -> f x [] in
+   - union_map f l acc =p= append (flatten (map g l)) acc
+ *)
+let union_map f l acc =
+  List.fold_left
+    (fun x y -> f y x)
+    acc
+    l
+
+(* A generic 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. *)
+
+let cartesian op l1 l2 =
+  map_append (fun x -> List.map (op x) l2) l1
+
+(* [cartesians] is an n-ary cartesian product: it iterates
+   [cartesian] over a list of lists.  *)
+
+let cartesians op init ll =
+  List.fold_right (cartesian op) ll [init]
+
+(* 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 rec combine3 x y z = 
+  match x, y, z with
+  | [], [], [] -> []
+  | (x :: xs), (y :: ys), (z :: zs) ->
+      (x, y, z) :: combine3 xs ys zs
+  | _, _, _ -> raise (Invalid_argument "List.combine3")
+  
+(* Keep only those products that do not return None *)
+
+let cartesian_filter op l1 l2 =
+  map_append (fun x -> map_filter (op x) l2) l1
+
+(* Keep only those products that do not return None *)
+
+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 = function
+  | (a,b)::l ->
+      let al,l' = split_by (fun (a',b) -> a=a') l in
+      (a,(b::List.map snd al)) :: factorize_left l'
+  | [] ->
+      []
+
diff --git a/lib/cList.mli b/lib/cList.mli
new file mode 100644
index 0000000000..c530a20813
--- /dev/null
+++ b/lib/cList.mli
@@ -0,0 +1,188 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+
+(** FIXME: From OCaml 3.12 onwards, that would only be a [module type of] *)
+
+module type S =
+sig
+  val length : 'a list -> int
+  val hd : 'a list -> 'a
+  val tl : 'a list -> 'a list
+  val nth : 'a list -> int -> 'a
+  val rev : 'a list -> 'a list
+  val append : 'a list -> 'a list -> 'a list
+  val rev_append : 'a list -> 'a list -> 'a list
+  val concat : 'a list list -> 'a list
+  val flatten : 'a list list -> 'a list
+  val iter : ('a -> unit) -> 'a list -> unit
+  val map : ('a -> 'b) -> 'a list -> 'b list
+  val rev_map : ('a -> 'b) -> 'a list -> 'b list
+  val fold_left : ('a -> 'b -> 'a) -> 'a -> 'b list -> 'a
+  val fold_right : ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b
+  val iter2 : ('a -> 'b -> unit) -> 'a list -> 'b list -> unit
+  val map2 : ('a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list
+  val rev_map2 : ('a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list
+  val fold_left2 : ('a -> 'b -> 'c -> 'a) -> 'a -> 'b list -> 'c list -> 'a
+  val fold_right2 : ('a -> 'b -> 'c -> 'c) -> 'a list -> 'b list -> 'c -> 'c
+  val for_all : ('a -> bool) -> 'a list -> bool
+  val exists : ('a -> bool) -> 'a list -> bool
+  val for_all2 : ('a -> 'b -> bool) -> 'a list -> 'b list -> bool
+  val exists2 : ('a -> 'b -> bool) -> 'a list -> 'b list -> bool
+  val mem : 'a -> 'a list -> bool
+  val memq : 'a -> 'a list -> bool
+  val find : ('a -> bool) -> 'a list -> 'a
+  val filter : ('a -> bool) -> 'a list -> 'a list
+  val find_all : ('a -> bool) -> 'a list -> 'a list
+  val partition : ('a -> bool) -> 'a list -> 'a list * 'a list
+  val assoc : 'a -> ('a * 'b) list -> 'b
+  val assq : 'a -> ('a * 'b) list -> 'b
+  val mem_assoc : 'a -> ('a * 'b) list -> bool
+  val mem_assq : 'a -> ('a * 'b) list -> bool
+  val remove_assoc : 'a -> ('a * 'b) list -> ('a * 'b) list
+  val remove_assq : 'a -> ('a * 'b) list -> ('a * 'b) list
+  val split : ('a * 'b) list -> 'a list * 'b list
+  val combine : 'a list -> 'b list -> ('a * 'b) list
+  val sort : ('a -> 'a -> int) -> 'a list -> 'a list
+  val stable_sort : ('a -> 'a -> int) -> 'a list -> 'a list
+  val fast_sort : ('a -> 'a -> int) -> 'a list -> 'a list
+  val merge : ('a -> 'a -> int) -> 'a list -> 'a list -> 'a list
+end
+
+module type ExtS =
+sig
+  include S
+  val compare : ('a -> 'a -> int) -> 'a list -> 'a list -> int
+  val equal : ('a -> 'a -> bool) -> 'a list -> 'a list -> bool
+  val add_set : 'a -> 'a list -> 'a list
+  val eq_set : 'a list -> 'a list -> bool
+  val intersect : 'a list -> 'a list -> 'a list
+  val union : 'a list -> 'a list -> 'a list
+  val unionq : 'a list -> 'a list -> 'a list
+  val subtract : 'a list -> 'a list -> 'a list
+  val subtractq : 'a list -> 'a list -> 'a list
+
+  (** [tabulate f n] builds [[f 0; ...; f (n-1)]] *)
+  val tabulate : (int -> 'a) -> int -> 'a list
+  val make : int -> 'a -> 'a list
+  val assign : 'a list -> int -> 'a -> 'a list
+  val distinct : 'a list -> bool
+  val duplicates : 'a list -> 'a list
+  val filter2 : ('a -> 'b -> bool) -> 'a list * 'b list -> 'a list * 'b list
+  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 filter_along : ('a -> bool) -> 'a list -> 'b list -> 'b list
+
+  (** [smartmap f [a1...an] = List.map f [a1...an]] but if for all i
+    [ f ai == ai], then [smartmap f l==l] *)
+  val smartmap : ('a -> 'a) -> 'a list -> 'a list
+  val map_left : ('a -> 'b) -> 'a list -> 'b list
+  val map_i : (int -> 'a -> 'b) -> int -> 'a list -> 'b list
+  val map2_i :
+    (int -> 'a -> 'b -> 'c) -> int -> 'a list -> 'b list -> 'c list
+  val map3 :
+    ('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 map_to_array : ('a -> 'b) -> 'a list -> 'b array
+  val filter_i :
+    (int -> 'a -> bool) -> 'a list -> 'a list
+
+  (** [smartfilter f [a1...an] = List.filter f [a1...an]] but if for all i
+    [f ai = true], then [smartfilter f l==l] *)
+  val smartfilter : ('a -> bool) -> 'a list -> 'a list
+
+  (** [index] returns the 1st index of an element in a list (counting from 1) *)
+  val index : 'a -> 'a list -> int
+  val index_f : ('a -> 'a -> bool) -> 'a -> 'a list -> int
+
+  (** [unique_index x l] returns [Not_found] if [x] doesn't occur exactly once *)
+  val unique_index : 'a -> 'a list -> int
+
+  (** [index0] behaves as [index] except that it starts counting at 0 *)
+  val index0 : 'a -> 'a list -> int
+  val index0_f : ('a -> 'a -> bool) -> 'a -> 'a list -> int
+  val iter3 : ('a -> 'b -> 'c -> unit) -> 'a list -> 'b list -> 'c list -> unit
+  val iter_i :  (int -> 'a -> unit) -> 'a list -> unit
+  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
+  val fold_right_and_left :
+      ('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 for_all_i : (int -> 'a -> bool) -> int -> 'a list -> bool
+  val except : 'a -> 'a list -> 'a list
+  val remove : 'a -> 'a list -> 'a list
+  val remove_first : 'a -> 'a list -> 'a list
+  val remove_assoc_in_triple : 'a -> ('a * 'b * 'c) list -> ('a * 'b * 'c) list
+  val assoc_snd_in_triple : 'a -> ('a * 'b * 'c) list -> 'b
+  val for_all2eq : ('a -> 'b -> bool) -> 'a list -> 'b list -> bool
+  val sep_last : 'a list -> 'a * 'a list
+  val try_find_i : (int -> 'a -> 'b) -> int -> 'a list -> 'b
+  val try_find : ('a -> 'b) -> 'a list -> 'b
+  val uniquize : 'a list -> 'a list
+
+  (** merges two sorted lists and preserves the uniqueness property: *)
+  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
+  (* former [split_at] was a duplicate of [chop] *)
+  val split_when : ('a -> bool) -> 'a list -> 'a list * 'a list
+  val split_by : ('a -> bool) -> 'a list -> 'a list * 'a list
+  val split3 : ('a * 'b * 'c) list -> 'a list * 'b list * 'c list
+  val partition_by : ('a -> 'a -> bool) -> 'a list -> 'a list list
+  val firstn : int -> 'a list -> 'a list
+  val last : 'a list -> 'a
+  val lastn : 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 list -> 'a list -> bool
+
+  (** [drop_prefix p l] returns [t] if [l=p++t] else return [l] *)
+  val drop_prefix : 'a list -> 'a list -> 'a list
+  val drop_last : 'a list -> 'a list
+
+  (** [map_append f [x1; ...; xn]] returns [(f x1)@(f x2)@...@(f xn)] *)
+  val map_append : ('a -> 'b list) -> 'a list -> 'b list
+  val join_map : ('a -> 'b list) -> 'a list -> 'b list
+
+  (** raises [Invalid_argument] if the two lists don't have the same length *)
+  val map_append2 : ('a -> 'b -> 'c list) -> 'a list -> 'b list -> 'c list
+  val share_tails : 'a list -> 'a list -> 'a list * 'a list * 'a list
+
+  (** [fold_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 fold_map : ('a -> 'b -> 'a * 'c) -> 'a -> 'b list -> 'a * 'c list
+  val fold_map' : ('b -> 'a -> 'c * 'a) -> 'b list -> 'a -> 'c list * 'a
+  val map_assoc : ('a -> 'b) -> ('c * 'a) list -> ('c * 'b) list
+  val assoc_f : ('a -> 'a -> bool) -> 'a -> ('a * 'b) list -> 'b
+
+  (** A generic 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 cartesian : ('a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list
+
+  (** [cartesians] is an n-ary cartesian product: it iterates
+    [cartesian] over a list of lists.  *)
+  val cartesians : ('a -> 'b -> 'b) -> 'b -> 'a list list -> 'b list
+
+  (** combinations [[a;b];[c;d]] returns [[a;c];[a;d];[b;c];[b;d]] *)
+  val combinations : 'a list list -> 'a list list
+  val combine3 : 'a list -> 'b list -> 'c list -> ('a * 'b * 'c) list
+
+  (** Keep only those products that do not return None *)
+  val cartesian_filter :
+    ('a -> 'b -> 'c option) -> 'a list -> 'b list -> 'c list
+  val cartesians_filter :
+    ('a -> 'b -> 'b option) -> 'b -> 'a list list -> 'b list
+
+  val union_map : ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b
+  val factorize_left : ('a * 'b) list -> ('a * 'b list) list
+end
+
+include ExtS
diff --git a/lib/clib.mllib b/lib/clib.mllib
index 5974fe5177..5b0e14f1ed 100644
--- a/lib/clib.mllib
+++ b/lib/clib.mllib
@@ -4,6 +4,7 @@ Coq_config
 Segmenttree
 Unicodetable
 Deque
+CList
 Util
 Serialize
 Xml_utils
diff --git a/lib/gmapl.ml b/lib/gmapl.ml
index 3c89ea68d2..5e8f27dc79 100644
--- a/lib/gmapl.ml
+++ b/lib/gmapl.ml
@@ -20,7 +20,7 @@ let fold = Gmap.fold
 let add x y m =
   try
     let l = Gmap.find x m in
-    Gmap.add x (y::list_except y l) m
+    Gmap.add x (y::List.except y l) m
   with Not_found ->
     Gmap.add x [y] m
 
@@ -29,6 +29,6 @@ let find x m =
 
 let remove x y m =
   let l = Gmap.find x m in
-  Gmap.add x (if List.mem y l then list_subtract l [y] else l) m
+  Gmap.add x (if List.mem y l then List.subtract l [y] else l) m
 
 
diff --git a/lib/util.ml b/lib/util.ml
index 1365f53cef..8916400ace 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -363,536 +363,7 @@ let ascii_of_ident s =
     done with End_of_input -> () end;
     !out
 
-(* Lists *)
-
-let rec list_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 -> list_compare cmp l1 l2
-	   | c -> c)
-
-let rec list_equal cmp l1 l2 =
-  l1 == l2 ||
-  match l1, l2 with
-    | [], [] -> true
-    | x1 :: l1, x2 :: l2 ->
-      cmp x1 x2 && list_equal cmp l1 l2
-    | _ -> false
-
-let list_intersect l1 l2 =
-  List.filter (fun x -> List.mem x l2) l1
-
-let list_union l1 l2 =
-  let rec urec = function
-    | [] -> l2
-    | a::l -> if List.mem a l2 then urec l else a::urec l
-  in
-  urec l1
-
-let list_unionq l1 l2 =
-  let rec urec = function
-    | [] -> l2
-    | a::l -> if List.memq a l2 then urec l else a::urec l
-  in
-  urec l1
-
-let list_subtract l1 l2 =
-  if l2 = [] then l1 else List.filter (fun x -> not (List.mem x l2)) l1
-
-let list_subtractq l1 l2 =
-  if l2 = [] then l1 else List.filter (fun x -> not (List.memq x l2)) l1
-
-let list_tabulate f len =
-  let rec tabrec n =
-    if n = len then [] else (f n)::(tabrec (n+1))
-  in
-  tabrec 0
-
-let list_addn n v =
-  let rec aux n l =
-    if n = 0 then l
-    else aux (pred n) (v::l)
-  in
-    if n < 0 then invalid_arg "list_addn"
-    else aux n
-
-let list_make n v = list_addn n v []
-
-let list_assign l n e =
-  let rec assrec stk = function
-    | ((h::t), 0) -> List.rev_append stk (e::t)
-    | ((h::t), n) -> assrec (h::stk) (t, n-1)
-    | ([], _) -> failwith "list_assign"
-  in
-  assrec [] (l,n)
-
-let rec list_smartmap f l = match l with
-    [] -> l
-  | h::tl ->
-      let h' = f h and tl' = list_smartmap f tl in
-	if h'==h && tl'==tl then l
-	else h'::tl'
-
-let list_map_left f = (* ensures the order in case of side-effects *)
-  let rec map_rec = function
-    | [] -> []
-    | x::l -> let v = f x in v :: map_rec l
-  in
-  map_rec
-
-let list_map_i f =
-  let rec map_i_rec i = function
-    | [] -> []
-    | x::l -> let v = f i x in v :: map_i_rec (i+1) l
-  in
-  map_i_rec
-
-let list_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)
-    | (_, _) -> invalid_arg "map2_i"
-  in
-  map_i i (l1,l2)
-
-let list_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 list_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 list_map_to_array f l =
-  Array.of_list (List.map f l)
-
-let rec list_smartfilter f l = match l with
-    [] -> l
-  | h::tl ->
-      let tl' = list_smartfilter f tl in
-	if f h then
-	  if tl' == tl then l
-	  else h :: tl'
-	else tl'
-	  
-let list_index_f f x =
-  let rec index_x n = function
-    | y::l -> if f x y then n else index_x (succ n) l
-    | [] -> raise Not_found
-  in
-  index_x 1
-
-let list_index0_f f x l = list_index_f f x l - 1
-
-let list_index x =
-  let rec index_x n = function
-    | y::l -> if x = y then n else index_x (succ n) l
-    | [] -> raise Not_found
-  in
-  index_x 1
-
-let list_index0 x l = list_index x l - 1
-
-let list_unique_index x =
-  let rec index_x n = function
-    | y::l ->
-	if x = y then
-	  if List.mem x l then raise Not_found
-	  else n
-	else index_x (succ n) l
-    | [] -> raise Not_found
-  in index_x 1
-
-let list_fold_right_i f i l =
-  let rec it_list_f i l a = match l with
-    | [] -> a
-    | b::l -> f (i-1) b (it_list_f (i-1) l a)
-  in
-  it_list_f (List.length l + i) l
-
-let list_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
-  in
-  it_list_f
-
-let rec list_fold_left3 f accu l1 l2 l3 =
-  match (l1, l2, l3) with
-    ([], [], []) -> accu
-  | (a1::l1, a2::l2, a3::l3) -> list_fold_left3 f (f accu a1 a2 a3) l1 l2 l3
-  | (_, _, _) -> invalid_arg "list_fold_left3"
-
-(* [list_fold_right_and_left f [a1;...;an] hd =
-   f (f (... (f (f hd
-                   an
-                   [an-1;...;a1])
-              an-1
-              [an-2;...;a1])
-         ...)
-        a2
-        [a1])
-     a1
-     []] *)
-
-let list_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
-
-let list_iter3 f l1 l2 l3 =
-  let rec iter = function
-    | ([], [], []) -> ()
-    | ((h1::t1), (h2::t2), (h3::t3)) -> f h1 h2 h3; iter (t1,t2,t3)
-    | (_, _, _) -> invalid_arg "map3"
-  in
-  iter (l1,l2,l3)
-
-let list_iter_i f l = list_fold_left_i (fun i _ x -> f i x) 0 () l
-
-let list_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 list_except x l = List.filter (fun y -> not (x = y)) l
-
-let list_remove = list_except (* Alias *)
-
-let rec list_remove_first a = function
-  | b::l when a = b -> l
-  | b::l -> b::list_remove_first a l
-  | [] -> raise Not_found
-
-let rec list_remove_assoc_in_triple x = function
-  | [] -> []
-  | (y,_,_ as z)::l -> if x = y then l else z::list_remove_assoc_in_triple x l
-
-let rec list_assoc_snd_in_triple x = function
-    [] -> raise Not_found
-  | (a,b,_)::l -> if compare a x = 0 then b else list_assoc_snd_in_triple x l
-
-let list_add_set x l = if List.mem x l then l else x::l
-
-let list_eq_set l1 l2 =
-  let rec aux l1 = function
-  | [] -> l1 = []
-  | a::l2 -> aux (list_remove_first a l1) l2 in
-  try aux l1 l2 with Not_found -> false
-
-let list_for_all2eq f l1 l2 =
-  try List.for_all2 f l1 l2 with Invalid_argument _ -> false
-
-let list_filter_i 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 rec list_sep_last = function
-  | [] -> failwith "sep_last"
-  | hd::[] -> (hd,[])
-  | hd::tl -> let (l,tl) = list_sep_last tl in (l,hd::tl)
-
-let list_try_find_i f =
-  let rec try_find_f n = function
-    | [] -> failwith "try_find_i"
-    | h::t -> try f n h with Failure _ -> try_find_f (n+1) t
-  in
-  try_find_f
-
-let list_try_find f =
-  let rec try_find_f = function
-    | [] -> failwith "try_find"
-    | h::t -> try f h with Failure _ -> try_find_f t
-  in
-  try_find_f
-
-let list_uniquize l =
-  let visited = Hashtbl.create 23 in
-  let rec aux acc = function
-    | h::t -> if Hashtbl.mem visited h then aux acc t else
-	  begin
-	    Hashtbl.add visited h h;
-	    aux (h::acc) t
-	  end
-    | [] -> List.rev acc
-  in aux [] l
-
-let list_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 rec list_merge_uniq cmp l1 l2 =
-  match l1, l2 with
-  | [], l2 -> l2
-  | l1, [] -> l1
-  | h1 :: t1, h2 :: t2 ->
-      let c = cmp h1 h2 in
-      if c = 0
-      then h1 :: list_merge_uniq cmp t1 t2
-      else if c <= 0
-      then h1 :: list_merge_uniq cmp t1 l2
-      else h2 :: list_merge_uniq cmp l1 t2
-
-let rec list_duplicates = function
-  | [] -> []
-  | x::l ->
-      let l' = list_duplicates l in
-      if List.mem x l then list_add_set x l' else l'
-
-let rec list_filter2 f = function
-  | [], [] as p -> p
-  | d::dp, l::lp ->
-     let (dp',lp' as p) = list_filter2 f (dp,lp) in
-      if f d l then d::dp', l::lp' else p
-  | _ -> invalid_arg "list_filter2"
-
-let rec list_map_filter f = function
-  | [] -> []
-  | x::l ->
-      let l' = list_map_filter f l in
-      match f x with None -> l' | Some y -> y::l'
-
-let list_map_filter_i f =
-  let rec aux i = function
-    | [] -> []
-    | x::l ->
-      let l' = aux (succ i) l in
-	match f i x with None -> l' | Some y -> y::l'
-  in aux 0
-
-let list_filter_along f filter l =
-  snd (list_filter2 (fun b c -> f b) (filter,l))
-
-let list_filter_with filter l =
-  list_filter_along (fun x -> x) filter l
-
-let list_subset l1 l2 =
-  let t2 = Hashtbl.create 151 in
-  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
-  in
-  look l1
-
-(* [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]  *)
-
-let list_chop n l =
-  let rec chop_aux i acc = function
-    | tl when i=0 -> (List.rev acc, tl)
-    | h::t -> chop_aux (pred i) (h::acc) t
-    | [] -> failwith "list_chop"
-  in
-  chop_aux n [] l
-
-(* [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 *)
-let list_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
-  in
-  split_when_loop []
-
-(* [list_split_by p l] splits [l] into two lists [(l1,l2)] such that elements of
-   [l1] satisfy [p] and elements of [l2] do not; order is preserved *)
-let list_split_by p =
-  let rec split_by_loop = function
-  | []   -> ([],[])
-  | a::l ->
-      let (l1,l2) = split_by_loop l in if p a then (a::l1,l2) else (l1,a::l2)
-  in
-  split_by_loop
-
-let rec list_split3 = function
-  | [] -> ([], [], [])
-  | (x,y,z)::l ->
-      let (rx, ry, rz) = list_split3 l in (x::rx, y::ry, z::rz)
-
-let rec list_insert_in_class f a = function
-  | [] -> [[a]]
-  | (b::_ as l)::classes when f a b -> (a::l)::classes
-  | l::classes -> l :: list_insert_in_class f a classes
-
-let list_partition_by f l =
-  List.fold_right (list_insert_in_class f) l []
-
-let list_firstn n l =
-  let rec aux acc = function
-    | (0, l) -> List.rev acc
-    | (n, (h::t)) -> aux (h::acc) (pred n, t)
-    | _ -> failwith "firstn"
-  in
-  aux [] (n,l)
-
-let rec list_last = function
-  | [] -> failwith "list_last"
-  | [x] -> x
-  | _ :: l -> list_last l
-
-let list_lastn n l =
-  let len = List.length l in
-  let rec aux m l =
-    if m = n then l else aux (m - 1) (List.tl l)
-  in
-  if len < n then failwith "lastn" else aux len l
-
-let rec list_skipn n l = match n,l with
-  | 0, _ -> l
-  | _, [] -> failwith "list_skipn"
-  | n, _::l -> list_skipn (pred n) l
-
-let list_skipn_at_least n l =
-  try list_skipn n l with Failure _ -> []
-
-let list_prefix_of prefl l =
-  let rec prefrec = function
-    | (h1::t1, h2::t2) -> h1 = h2 && prefrec (t1,t2)
-    | ([], _) -> true
-    | (_, _) -> false
-  in
-    prefrec (prefl,l)
-
-let list_drop_prefix p l =
-(* if l=p++t then return t else l *)
-  let rec list_drop_prefix_rec = function
-    | ([], tl) -> Some tl
-    | (_, []) -> None
-    | (h1::tp, h2::tl) ->
-	if h1 = h2 then list_drop_prefix_rec (tp,tl) else None
-  in
-    match list_drop_prefix_rec (p,l) with
-      | Some r -> r
-      | None -> l
-
-let list_map_append f l = List.flatten (List.map f l)
-let list_join_map = list_map_append   (* Alias *)
-
-let list_map_append2 f l1 l2 = List.flatten (List.map2 f l1 l2)
-
-let list_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)
-  in
-  shr_rev [] (List.rev l1, List.rev l2)
-
-let rec list_fold_map f e = function
-  |  []  -> (e,[])
-  |  h::t ->
-       let e',h' = f e h in
-       let e'',t' = list_fold_map f e' t in
-         e'',h'::t'
-
-(* (* tail-recursive version of the above function *)
-let list_fold_map f e l =
-  let g (e,b') h =
-    let (e',h') = f e h in
-      (e',h'::b')
-  in
-  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 list_fold_map' f l e =
-  List.fold_right (fun x (l,e) -> let (y,e) = f x e in (y::l,e)) l ([],e)
-
-let list_map_assoc f = List.map (fun (x,a) -> (x,f a))
-
-let rec list_assoc_f f a = function
-  | (x, e) :: xs -> if f a x then e else list_assoc_f f a xs
-  | [] -> raise Not_found
-
-(* Specification:
-   - =p= is set equality (double inclusion)
-   - f such that \forall l acc, (f l acc) =p= append (f l []) acc
-   - let g = fun x -> f x [] in
-   - union_map f l acc =p= append (flatten (map g l)) acc
- *)
-let list_union_map f l acc =
-  List.fold_left
-    (fun x y -> f y x)
-    acc
-    l
-
-(* A generic cartesian product: for any operator (**),
-   [list_cartesian (**) [x1;x2] [y1;y2] = [x1**y1; x1**y2; x2**y1; x2**y1]],
-   and so on if there are more elements in the lists. *)
-
-let list_cartesian op l1 l2 =
-  list_map_append (fun x -> List.map (op x) l2) l1
-
-(* [list_cartesians] is an n-ary cartesian product: it iterates
-   [list_cartesian] over a list of lists.  *)
-
-let list_cartesians op init ll =
-  List.fold_right (list_cartesian op) ll [init]
-
-(* list_combinations [[a;b];[c;d]] gives [[a;c];[a;d];[b;c];[b;d]] *)
-
-let list_combinations l = list_cartesians (fun x l -> x::l) [] l
-
-let rec list_combine3 x y z = 
-  match x, y, z with
-  | [], [], [] -> []
-  | (x :: xs), (y :: ys), (z :: zs) ->
-      (x, y, z) :: list_combine3 xs ys zs
-  | _, _, _ -> raise (Invalid_argument "list_combine3")
-  
-(* Keep only those products that do not return None *)
-
-let list_cartesian_filter op l1 l2 =
-  list_map_append (fun x -> list_map_filter (op x) l2) l1
-
-(* Keep only those products that do not return None *)
-
-let list_cartesians_filter op init ll =
-  List.fold_right (list_cartesian_filter op) ll [init]
-
-(* Drop the last element of a list *)
-
-let rec list_drop_last = function [] -> assert false | hd :: [] -> [] | hd :: tl -> hd :: list_drop_last tl
-
-(* Factorize lists of pairs according to the left argument *)
-let rec list_factorize_left = function
-  | (a,b)::l ->
-      let al,l' = list_split_by (fun (a',b) -> a=a') l in
-      (a,(b::List.map snd al)) :: list_factorize_left l'
-  | [] ->
-      []
+module List : CList.ExtS = CList
 
 (* Arrays *)
 
@@ -1212,10 +683,10 @@ let array_rev_to_list a =
   tolist 0 []
 
 let array_filter_along f filter v =
-  Array.of_list (list_filter_along f filter (Array.to_list v))
+  Array.of_list (CList.filter_along f filter (Array.to_list v))
 
 let array_filter_with filter v =
-  Array.of_list (list_filter_with filter (Array.to_list v))
+  Array.of_list (CList.filter_with filter (Array.to_list v))
 
 (* Matrices *)
 
diff --git a/lib/util.mli b/lib/util.mli
index 43d8ea1b0a..a8ea6854c1 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -71,133 +71,7 @@ val ascii_of_ident : string -> string
 
 (** {6 Lists. } *)
 
-val list_compare : ('a -> 'a -> int) -> 'a list -> 'a list -> int
-val list_equal : ('a -> 'a -> bool) -> 'a list -> 'a list -> bool
-val list_add_set : 'a -> 'a list -> 'a list
-val list_eq_set : 'a list -> 'a list -> bool
-val list_intersect : 'a list -> 'a list -> 'a list
-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
-
-(** [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
-val list_assign : 'a list -> int -> 'a -> 'a list
-val list_distinct : 'a list -> bool
-val list_duplicates : 'a list -> 'a list
-val list_filter2 : ('a -> 'b -> bool) -> 'a list * 'b list -> 'a list * 'b list
-val list_map_filter : ('a -> 'b option) -> 'a list -> 'b list
-val list_map_filter_i : (int -> 'a -> 'b option) -> 'a list -> 'b list
-val list_filter_with : bool list -> 'a list -> 'a list
-val list_filter_along : ('a -> bool) -> 'a list -> 'b list -> 'b list
-
-(** [list_smartmap f [a1...an] = List.map f [a1...an]] but if for all i
-   [ f ai == ai], then [list_smartmap f l==l] *)
-val list_smartmap : ('a -> 'a) -> 'a list -> 'a list
-val list_map_left : ('a -> 'b) -> 'a list -> 'b list
-val list_map_i : (int -> 'a -> 'b) -> int -> 'a list -> 'b list
-val list_map2_i :
-  (int -> 'a -> 'b -> 'c) -> int -> 'a list -> 'b list -> 'c list
-val list_map3 :
-  ('a -> 'b -> 'c -> 'd) -> 'a list -> 'b list -> 'c list -> 'd list
-val list_map4 :
-  ('a -> 'b -> 'c -> 'd -> 'e) -> 'a list -> 'b list -> 'c list -> 'd list -> 'e list
-val list_map_to_array : ('a -> 'b) -> 'a list -> 'b array
-val list_filter_i :
-  (int -> 'a -> bool) -> 'a list -> 'a list
-
-(** [list_smartfilter f [a1...an] = List.filter f [a1...an]] but if for all i
-   [f ai = true], then [list_smartfilter f l==l] *)
-val list_smartfilter : ('a -> bool) -> 'a list -> 'a list
-
-(** [list_index] returns the 1st index of an element in a list (counting from 1) *)
-val list_index : 'a -> 'a list -> int
-val list_index_f : ('a -> 'a -> bool) -> 'a -> 'a list -> int
-
-(** [list_unique_index x l] returns [Not_found] if [x] doesn't occur exactly once *)
-val list_unique_index : 'a -> 'a list -> int
-
-(** [list_index0] behaves as [list_index] except that it starts counting at 0 *)
-val list_index0 : 'a -> 'a list -> int
-val list_index0_f : ('a -> 'a -> bool) -> 'a -> 'a list -> int
-val list_iter3 : ('a -> 'b -> 'c -> unit) -> 'a list -> 'b list -> 'c list -> unit
-val list_iter_i :  (int -> 'a -> unit) -> 'a list -> unit
-val list_fold_right_i :  (int -> 'a -> 'b -> 'b) -> int -> 'a list -> 'b -> 'b
-val list_fold_left_i :  (int -> 'a -> 'b -> 'a) -> int -> 'a -> 'b list -> 'a
-val list_fold_right_and_left :
-    ('a -> 'b -> 'b list -> 'a) -> 'b list -> 'a -> 'a
-val list_fold_left3 : ('a -> 'b -> 'c -> 'd -> 'a) -> 'a -> 'b list -> 'c list -> 'd list -> 'a
-val list_for_all_i : (int -> 'a -> bool) -> int -> 'a list -> bool
-val list_except : 'a -> 'a list -> 'a list
-val list_remove : 'a -> 'a list -> 'a list
-val list_remove_first : 'a -> 'a list -> 'a list
-val list_remove_assoc_in_triple : 'a -> ('a * 'b * 'c) list -> ('a * 'b * 'c) list
-val list_assoc_snd_in_triple : 'a -> ('a * 'b * 'c) list -> 'b
-val list_for_all2eq : ('a -> 'b -> bool) -> 'a list -> 'b list -> bool
-val list_sep_last : 'a list -> 'a * 'a list
-val list_try_find_i : (int -> 'a -> 'b) -> int -> 'a list -> 'b
-val list_try_find : ('a -> 'b) -> 'a list -> 'b
-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_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_split_by : ('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
-val list_firstn : int -> 'a list -> 'a list
-val list_last : 'a list -> 'a
-val list_lastn : int -> 'a list -> 'a list
-val list_skipn : int -> 'a list -> 'a list
-val list_skipn_at_least : int -> 'a list -> 'a list
-val list_addn : int -> 'a -> 'a list -> 'a list
-val list_prefix_of : 'a list -> 'a list -> bool
-
-(** [list_drop_prefix p l] returns [t] if [l=p++t] else return [l] *)
-val list_drop_prefix : 'a list -> 'a list -> 'a list
-val list_drop_last : 'a list -> 'a list
-
-(** [map_append f [x1; ...; xn]] returns [(f x1)@(f x2)@...@(f xn)] *)
-val list_map_append : ('a -> 'b list) -> 'a list -> 'b list
-val list_join_map : ('a -> 'b list) -> 'a list -> 'b list
-
-(** raises [Invalid_argument] if the two lists don't have the same length *)
-val list_map_append2 : ('a -> 'b -> 'c list) -> 'a list -> 'b list -> 'c list
-val list_share_tails : 'a list -> 'a list -> 'a list * 'a list * 'a list
-
-(** [list_fold_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 list_fold_map : ('a -> 'b -> 'a * 'c) -> 'a -> 'b list -> 'a * 'c list
-val list_fold_map' : ('b -> 'a -> 'c * 'a) -> 'b list -> 'a -> 'c list * 'a
-val list_map_assoc : ('a -> 'b) -> ('c * 'a) list -> ('c * 'b) list
-val list_assoc_f : ('a -> 'a -> bool) -> 'a -> ('a * 'b) list -> 'b
-
-(** A generic cartesian product: for any operator (**),
-   [list_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 list_cartesian : ('a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list
-
-(** [list_cartesians] is an n-ary cartesian product: it iterates
-   [list_cartesian] over a list of lists.  *)
-val list_cartesians : ('a -> 'b -> 'b) -> 'b -> 'a list list -> 'b list
-
-(** list_combinations [[a;b];[c;d]] returns [[a;c];[a;d];[b;c];[b;d]] *)
-val list_combinations : 'a list list -> 'a list list
-val list_combine3 : 'a list -> 'b list -> 'c list -> ('a * 'b * 'c) list
-
-(** Keep only those products that do not return None *)
-val list_cartesian_filter :
-  ('a -> 'b -> 'c option) -> 'a list -> 'b list -> 'c list
-val list_cartesians_filter :
-  ('a -> 'b -> 'b option) -> 'b -> 'a list list -> 'b list
-
-val list_union_map : ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b
-val list_factorize_left : ('a * 'b) list -> ('a * 'b list) list
+module List : CList.ExtS
 
 (** {6 Arrays. } *)