Extract Coq lists to Caml lists.

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@929 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

13 files changed, 112 insertions, 146 deletions

diff --git a/caml/CMparser.mly b/caml/CMparser.mly
index 0b3eafd8..25fb0321 100644
--- a/caml/CMparser.mly
+++ b/caml/CMparser.mly
@@ -37,13 +37,13 @@ type rexpr =
 
 let temp_counter = ref 0
 
-let temporaries = ref Coq_nil
+let temporaries = ref []
 
 let mktemp () =
   incr temp_counter;
   let n = Printf.sprintf "__t%d" !temp_counter in
   let id = intern_string n in
-  temporaries := Coq_cons(id, !temporaries);
+  temporaries := id :: !temporaries;
   id
 
 let convert_accu = ref []
@@ -75,11 +75,11 @@ let rec convert_rexpr = function
       Evar t
 
 and convert_rexpr_list = function
-  | Coq_nil -> Coq_nil
-  | Coq_cons(e1, el) ->
+  | [] -> []
+  | e1 :: el ->
       let c1 = convert_rexpr e1 in
       let cl = convert_rexpr_list el in
-      Coq_cons(c1, cl)
+      c1 :: cl
 
 let rec prepend_seq stmts last =
   match stmts with
@@ -149,9 +149,9 @@ let mkswitch expr (cases, dfl) =
   convert_accu := [];
   let c = convert_rexpr expr in
   let rec mktable = function
-  | [] -> Coq_nil
+  | [] -> []
   | (key, exit) :: rem ->
-      Coq_cons(Coq_pair(coqint_of_camlint key, exitnum exit), mktable rem) in
+      Coq_pair(coqint_of_camlint key, exitnum exit) :: mktable rem in
   prepend_seq !convert_accu (Sswitch(c, mktable cases, exitnum dfl))
 
 (***
@@ -174,10 +174,10 @@ let mkmatch_aux expr cases =
   let ncases = Int32.of_int (List.length cases) in
   let rec mktable n = function
     | [] -> assert false
-    | [key, action] -> Coq_nil
+    | [key, action] -> []
     | (key, action) :: rem ->
-        Coq_cons(Coq_pair(coqint_of_camlint key, nat_of_camlint n),
-                 mktable (Int32.succ n) rem) in
+        Coq_pair(coqint_of_camlint key, nat_of_camlint n)
+        :: mktable (Int32.succ n) rem in
   let sw =
     Sswitch(expr, mktable 0l cases, nat_of_camlint (Int32.pred ncases)) in
   let rec mkblocks body n = function
@@ -329,20 +329,18 @@ prog:
 ;
 
 global_declarations:
-    /* empty */                                 { Coq_nil }
-  | global_declarations global_declaration      { Coq_cons($2, $1) }
+    /* empty */                                 { [] }
+  | global_declarations global_declaration      { $2 :: $1 }
 ;
 
 global_declaration:
     VAR STRINGLIT LBRACKET INTLIT RBRACKET
-      { Coq_pair(Coq_pair($2,
-                          Coq_cons(Init_space (z_of_camlint $4), Coq_nil)),
-                 ()) }
+      { Coq_pair(Coq_pair($2, [ Init_space (z_of_camlint $4) ]), ()) }
 ;
 
 proc_list:
-    /* empty */                                 { Coq_nil }
-  | proc_list proc                              { Coq_cons($2, $1) }
+    /* empty */                                 { [] }
+  | proc_list proc                              { $2 :: $1 }
 ;
 
 /* Procedures */
@@ -355,7 +353,7 @@ proc:
       stmt_list
     RBRACE
       { let tmp = !temporaries in
-        temporaries := Coq_nil;
+        temporaries := [];
         temp_counter := 0;
         Coq_pair($1,
         Internal { fn_sig = $6;
@@ -371,21 +369,21 @@ proc:
 
 signature:
     type_ 
-               { {sig_args = Coq_nil; sig_res = Some $1} }
+               { {sig_args = []; sig_res = Some $1} }
   | VOID
-               { {sig_args = Coq_nil; sig_res = None} }
+               { {sig_args = []; sig_res = None} }
   | type_ MINUSGREATER signature
-               { let s = $3 in {s with sig_args = Coq_cons($1, s.sig_args)} }
+               { let s = $3 in {s with sig_args = $1 :: s.sig_args} }
 ;
 
 parameters:
-    /* empty */                                 { Coq_nil }
+    /* empty */                                 { [] }
   | parameter_list                              { $1 }
 ;
 
 parameter_list:
-    IDENT                                       { Coq_cons($1, Coq_nil) }
-  | parameter_list COMMA IDENT                  { Coq_cons($3, $1) }
+    IDENT                                       { $1 :: [] }
+  | parameter_list COMMA IDENT                  { $3 :: $1 }
 ;
 
 stack_declaration:
@@ -394,7 +392,7 @@ stack_declaration:
 ;
 
 var_declarations:
-    /* empty */                                 { Coq_nil }
+    /* empty */                                 { [] }
   | var_declarations var_declaration            { CList.app $2 $1 }
 ;
 
@@ -514,13 +512,13 @@ expr:
 ;
 
 expr_list:
-    /* empty */                                 { Coq_nil }
+    /* empty */                                 { [] }
   | expr_list_1                                 { $1 }
 ;
 
 expr_list_1:
-    expr                     %prec COMMA        { Coq_cons($1, Coq_nil) }
-  | expr COMMA expr_list_1                      { Coq_cons($1, $3) }
+    expr                     %prec COMMA        { $1 :: [] }
+  | expr COMMA expr_list_1                      { $1 :: $3 }
 ;
 
 memory_chunk:
diff --git a/caml/CMtypecheck.ml b/caml/CMtypecheck.ml
index 1ac00654..d761f759 100644
--- a/caml/CMtypecheck.ml
+++ b/caml/CMtypecheck.ml
@@ -35,9 +35,7 @@ let tfloat = Base Tfloat
 
 let ty_of_typ = function Tint -> tint | Tfloat -> tfloat
 
-let rec ty_of_sig_args = function
-  | Coq_nil -> []
-  | Coq_cons(t, l) -> ty_of_typ t :: ty_of_sig_args l
+let ty_of_sig_args tyl = List.map ty_of_typ tyl
 
 let rec repr t =
   match t with
@@ -244,8 +242,8 @@ let rec type_expr env lenv e =
 
 and type_exprlist env lenv el =
   match el with
-  | Coq_nil -> []
-  | Coq_cons (e1, et) ->
+  | [] -> []
+  | e1 :: et ->
       let te1 = type_expr env lenv e1 in
       let tet = type_exprlist env lenv et in
       (te1 :: tet)
@@ -352,8 +350,8 @@ let rec type_stmt env blk ret s =
 
 let rec env_of_vars idl =
   match idl with
-  | Coq_nil -> []
-  | Coq_cons(id1, idt) -> (id1, newvar()) :: env_of_vars idt
+  | [] -> []
+  | id1 :: idt -> (id1, newvar()) :: env_of_vars idt
 
 let type_function id f =
   try
@@ -369,4 +367,4 @@ let type_fundef (Coq_pair (id, fd)) =
   | External ef -> ()
 
 let type_program p =
-  coqlist_iter type_fundef p.prog_funct; p
+  List.iter type_fundef p.prog_funct; p
diff --git a/caml/Camlcoq.ml b/caml/Camlcoq.ml
index e9089cf3..98fd79c8 100644
--- a/caml/Camlcoq.ml
+++ b/caml/Camlcoq.ml
@@ -77,25 +77,6 @@ let extern_atom a =
   with Not_found ->
     Printf.sprintf "<unknown atom %ld>" (camlint_of_positive a)
 
-(* Lists *)
-
-let rec coqlist_iter f = function
-    Coq_nil -> ()
-  | Coq_cons(a,l) -> f a; coqlist_iter f l
-
-let rec length_coqlist = function
-  | Coq_nil -> 0
-  | Coq_cons (x, l) -> 1 + length_coqlist l
-
-let array_of_coqlist = function
-  | Coq_nil -> [||]
-  | Coq_cons(hd, tl) as l ->
-      let a = Array.create (length_coqlist l) hd in
-      let rec fill i = function
-        | Coq_nil -> a
-        | Coq_cons(hd, tl) -> a.(i) <- hd; fill (i + 1) tl in
-      fill 1 tl
-
 (* Strings *)
 
 let char_of_ascii (Ascii.Ascii(a0, a1, a2, a3, a4, a5, a6, a7)) =
diff --git a/caml/Cil2Csyntax.ml b/caml/Cil2Csyntax.ml
index 7224610c..41fe1d4f 100644
--- a/caml/Cil2Csyntax.ml
+++ b/caml/Cil2Csyntax.ml
@@ -88,12 +88,6 @@ let rec getFieldType f = function
 
 (** ** Some functions over lists *)
 
-(** Apply [f] to each element of the OCaml list [l]
-    and build a Coq list with the results returned by [f] *)
-let rec map_coqlist f l = match l with
-  | [] -> CList.Coq_nil
-  | a :: b -> CList.Coq_cons (f a, map_coqlist f b)
-  
 (** Keep the elements in a list from [elt] (included) to the end
     (used for the translation of the [switch] statement) *)
 let rec keepFrom elt = function
@@ -111,13 +105,6 @@ let rec keepUntil elt' = function
 let keepBetween elt elt' l =
   keepUntil elt' (keepFrom elt l)
 
-(** Reverse-append over Coq lists *)
-
-let rec revappend l1 l2 =
-  match l1 with
-  | CList.Coq_nil -> l2
-  | CList.Coq_cons(hd, tl) -> revappend tl (CList.Coq_cons (hd, l2))
-
 (** ** Functions used to handle locations *)
 
 (** Update the current location *)
@@ -162,18 +149,18 @@ let typeStringLiteral s =
   Tarray(Tint(I8, Unsigned), z_of_camlint(Int32.of_int(String.length s + 1)))
 
 let global_for_string s id =
-  let init = ref CList.Coq_nil in
+  let init = ref [] in
   let add_char c =
-    init := CList.Coq_cons(
-       AST.Init_int8(coqint_of_camlint(Int32.of_int(Char.code c))),
-       !init) in
+    init :=
+       AST.Init_int8(coqint_of_camlint(Int32.of_int(Char.code c)))
+       :: !init in
   add_char '\000';
   for i = String.length s - 1 downto 0 do add_char s.[i] done;
   Datatypes.Coq_pair(Datatypes.Coq_pair(id, !init), typeStringLiteral s)
 
 let globals_for_strings globs =
   Hashtbl.fold
-    (fun s id l -> CList.Coq_cons(global_for_string s id, l))
+    (fun s id l -> global_for_string s id :: l)
     stringTable globs
 
 (** ** Handling of stubs for variadic functions *)
@@ -206,7 +193,7 @@ let declare_stub_function stub_name stub_type =
   | _ -> assert false
 
 let declare_stub_functions k =
-  Hashtbl.fold (fun n i k -> CList.Coq_cons(declare_stub_function n i, k))
+  Hashtbl.fold (fun n i k -> declare_stub_function n i :: k)
                stub_function_table k
 
 (** ** Generation of temporary variable names *)
@@ -346,13 +333,13 @@ and processCast t e =
 
 (** Convert a [Cil.exp list] into an [CamlCoq.exprlist] *)
 and processParamsE = function
-  | [] -> Coq_nil
+  | [] -> []
   | e :: l ->
       let (Expr (_, t)) as e' = convertExp e in
 	match t with
 	  | Tstruct _ | Tunion _ ->
               unsupported "function parameter of struct or union type"
-	  | _ -> Coq_cons (e', processParamsE l)
+	  | _ -> e' :: processParamsE l
 
 
 (** Convert a [Cil.exp] into a [CabsCoq.expr] *)
@@ -546,8 +533,8 @@ let convertExpFuncall e eList =
             | _ ->
                 unsupported "call to variadic function" in
           let rec typeOfExprList = function
-            | Coq_nil -> Tnil
-            | Coq_cons (Expr (_, ty), rem) -> Tcons (ty, typeOfExprList rem) in
+            | [] -> Tnil
+            | Expr (_, ty) :: rem -> Tcons (ty, typeOfExprList rem) in
           let targs = typeOfExprList params in
           let tres = convertTyp res in
           let (stub_fun_name, stub_fun_typ) =
@@ -742,8 +729,8 @@ let convertGFun fdec =
     | _ -> internal_error "convertGFun: incorrect function type"
   in
   let s = processStmtList fdec.sbody.bstmts in   (* function body -- do it first because of generated temps *)
-  let args = map_coqlist convertVarinfoParam fdec.sformals in   (* parameters*)
-  let varList = map_coqlist convertVarinfo fdec.slocals in   (* local vars *)
+  let args = List.map convertVarinfoParam fdec.sformals in   (* parameters*)
+  let varList = List.map convertVarinfo fdec.slocals in   (* local vars *)
   if v.vname = "main" then begin
     match ret with
     | Tint(_, _) -> ()
@@ -758,8 +745,8 @@ let convertGFun fdec =
 (** Auxiliary for [convertInit] *)
 
 let rec initDataLen accu = function
-  | CList.Coq_nil -> accu
-  | CList.Coq_cons(i1, il) ->
+  | [] -> accu
+  | i1 :: il ->
       let sz = match i1 with
       | Init_int8 _ -> 1l
       | Init_int16 _ -> 2l
@@ -811,19 +798,19 @@ let rec extract_constant e =
   | _ -> ICnone
 
 let init_data_of_string s =
-  let id = ref CList.Coq_nil in
+  let id = ref [] in
   let enter_char c =
     let n = coqint_of_camlint(Int32.of_int(Char.code c)) in
-    id := CList.Coq_cons(Init_int8 n, !id) in
+    id := Init_int8 n :: !id in
   enter_char '\000';
   for i = String.length s - 1 downto 0 do enter_char s.[i] done;
   !id
 
 let convertInit init =
-  let k = ref Coq_nil
+  let k = ref []
   and pos = ref 0 in
   let emit size datum =
-    k := Coq_cons(datum, !k);
+    k := datum :: !k;
     pos := !pos + size in
   let emit_space size =
     emit size (Init_space (z_of_camlint (Int32.of_int size))) in
@@ -886,7 +873,7 @@ let convertInit init =
 let convertInitInfo ty info =
   match info.init with
   | None -> 
-      CList.Coq_cons(Init_space(Csyntax.sizeof (convertTyp ty)), CList.Coq_nil)
+      [ Init_space(Csyntax.sizeof (convertTyp ty)) ]
   | Some init ->
       convertInit init
 
@@ -904,7 +891,7 @@ let convertGVar v i =
 let convertExtVar v =
   updateLoc(v.vdecl);
   let id = intern_string v.vname in
-  Datatypes.Coq_pair (Datatypes.Coq_pair(id, CList.Coq_nil),
+  Datatypes.Coq_pair (Datatypes.Coq_pair(id, []),
                       convertTyp v.vtype)
 
 (** Convert a [Cil.GVarDecl] into an external function declaration *)
@@ -923,7 +910,7 @@ let convertExtFun v =
     functions and the second component, of type [(ident * coq_type) coqlist],
     the definitions of the global variables of the program *)
 let rec processGlobals = function
-  | [] -> (CList.Coq_nil, CList.Coq_nil)
+  | [] -> ([], [])
   | g :: l ->
 	match g with
 	  | GType _ -> processGlobals l (* typedefs are unrolled... *)
@@ -940,24 +927,24 @@ let rec processGlobals = function
               | TFun (tres, Some targs, false, _) ->
                   let fn = convertExtFun v in
                   let (fList, vList) = processGlobals l in
-                  (CList.Coq_cons (fn, fList), vList)
+                  (fn :: fList, vList)
               | TFun (tres, _, _, _) ->
                   processGlobals l
               | _ ->
                   let var = convertExtVar v in
                   let (fList, vList) = processGlobals l in
-                  (fList, CList.Coq_cons (var, vList))
+                  (fList, var :: vList)
               end
 	  | GVar (v, init, loc) ->
 	      updateLoc(loc);
               let var = convertGVar v init in
               let (fList, vList) = processGlobals l in
-              (fList, CList.Coq_cons (var, vList))
+              (fList, var :: vList)
 	  | GFun (fdec, loc) ->
 	      updateLoc(loc);
               let fn = convertGFun fdec in
               let (fList, vList) = processGlobals l in
-              (CList.Coq_cons (fn, fList), vList)
+              (fn :: fList, vList)
 	  | GAsm (_, loc) ->
 	      updateLoc(loc);
               unsupported "inline assembly"
@@ -992,7 +979,7 @@ let convertFile f =
   let (funList, defList) = processGlobals (cleanupGlobals f.globals) in
   let funList' = declare_stub_functions funList in
   let funList'' = match f.globinit with
-    | Some fdec -> CList.Coq_cons (convertGFun fdec, funList')
+    | Some fdec -> convertGFun fdec :: funList'
     | None -> funList' in
   let defList' = globals_for_strings defList in
   { AST.prog_funct = funList'';
diff --git a/caml/Coloringaux.ml b/caml/Coloringaux.ml
index 984fbb34..f11738df 100644
--- a/caml/Coloringaux.ml
+++ b/caml/Coloringaux.ml
@@ -278,13 +278,13 @@ let class_of_type = function Tint -> 0 | Tfloat -> 1
 let num_register_classes = 2
 
 let caller_save_registers = [|
-  array_of_coqlist Conventions.int_caller_save_regs;
-  array_of_coqlist Conventions.float_caller_save_regs
+  Array.of_list Conventions.int_caller_save_regs;
+  Array.of_list Conventions.float_caller_save_regs
 |]
 
 let callee_save_registers = [|
-  array_of_coqlist Conventions.int_callee_save_regs;
-  array_of_coqlist Conventions.float_callee_save_regs
+  Array.of_list Conventions.int_callee_save_regs;
+  Array.of_list Conventions.float_callee_save_regs
 |]
 
 let num_available_registers = 
diff --git a/caml/Driver.ml b/caml/Driver.ml
index dacc9dcb..8fffcaa0 100644
--- a/caml/Driver.ml
+++ b/caml/Driver.ml
@@ -39,7 +39,7 @@ let print_error oc msg =
   let print_one_error = function
   | Errors.MSG s -> output_string oc (Camlcoq.camlstring_of_coqstring s)
   | Errors.CTX i -> output_string oc (Camlcoq.extern_atom i)
-  in Camlcoq.coqlist_iter print_one_error msg
+  in List.iter print_one_error msg
 
 (* For the CIL -> Csyntax translator:
 
diff --git a/caml/Linearizeaux.ml b/caml/Linearizeaux.ml
index 02a95241..2f2333fb 100644
--- a/caml/Linearizeaux.ml
+++ b/caml/Linearizeaux.ml
@@ -51,14 +51,14 @@ let rec pos_of_int n =
 module IntSet = Set.Make(struct type t = int let compare = compare end)
 
 let enumerate_aux f reach =
-  let enum = ref Coq_nil in
+  let enum = ref [] in
   let emitted = Array.make (int_of_pos f.fn_nextpc) false in
   let rec emit_block pending pc =
     let npc = int_of_pos pc in
     if emitted.(npc)
     then emit_restart pending
     else begin
-      enum := Coq_cons(pc, !enum);
+      enum := pc :: !enum;
       emitted.(npc) <- true;
       match PTree.get pc f.fn_code with
       | None -> assert false
diff --git a/caml/PrintCsyntax.ml b/caml/PrintCsyntax.ml
index 6aaa5397..bb25339a 100644
--- a/caml/PrintCsyntax.ml
+++ b/caml/PrintCsyntax.ml
@@ -205,8 +205,8 @@ and print_expr_prec p (context_prec, e) =
 
 let rec print_expr_list p (first, el) =
   match el with
-  | Coq_nil -> ()
-  | Coq_cons(e1, et) ->
+  | [] -> ()
+  | e1 :: et ->
       if not first then fprintf p ",@ ";
       print_expr p e1;
       print_expr_list p (false, et)
@@ -305,12 +305,12 @@ let name_function_parameters fun_name params =
   Buffer.add_string b fun_name;
   Buffer.add_char b '(';
   begin match params with
-  | Coq_nil ->
+  | [] ->
       Buffer.add_string b "void"
   | _ ->
       let rec add_params first = function
-      | Coq_nil -> ()
-      | Coq_cons(Coq_pair(id, ty), rem) ->
+      | [] -> ()
+      | Coq_pair(id, ty) :: rem ->
           if not first then Buffer.add_string b ", ";
           Buffer.add_string b (name_cdecl (extern_atom id) ty);
           add_params false rem in
@@ -325,7 +325,7 @@ let print_function p id f =
                                                   f.fn_params)
                         f.fn_return);
   fprintf p "@[<v 2>{@ ";
-  coqlist_iter
+  List.iter
     (fun (Coq_pair(id, ty)) ->
       fprintf p "%s;@ " (name_cdecl (extern_atom id) ty))
     f.fn_vars;
@@ -342,9 +342,9 @@ let print_fundef p (Coq_pair(id, fd)) =
 
 let string_of_init id =
   try
-    let s = String.create (length_coqlist id) in
+    let s = String.create (List.length id) in
     let i = ref 0 in
-    coqlist_iter
+    List.iter
       (function
         | Init_int8 n ->
             s.[!i] <- Char.chr(Int32.to_int(camlint_of_coqint n));
@@ -382,16 +382,16 @@ let print_init p = function
 
 let print_globvar p (Coq_pair(Coq_pair(id, init), ty)) =
   match init with
-  | Coq_nil ->
+  | [] ->
       fprintf p "extern %s;@ @ "
               (name_cdecl (extern_atom id) ty)
-  | Coq_cons(Init_space _, Coq_nil) ->
+  | [Init_space _] ->
       fprintf p "%s;@ @ "
               (name_cdecl (extern_atom id) ty)
   | _ ->
       fprintf p "@[<hov 2>%s = {@ "
               (name_cdecl (extern_atom id) ty);
-      coqlist_iter (print_init p) init;
+      List.iter (print_init p) init;
       fprintf p "};@]@ @ "
 
 (* Collect struct and union types *)
@@ -432,8 +432,8 @@ let rec collect_expr (Expr(ed, ty)) =
   | Efield(e1, id) -> collect_expr e1
 
 let rec collect_expr_list = function
-  | Coq_nil -> ()
-  | Coq_cons(hd, tl) -> collect_expr hd; collect_expr_list tl
+  | [] -> ()
+  | hd :: tl -> collect_expr hd; collect_expr_list tl
 
 let rec collect_stmt = function
   | Sskip -> ()
@@ -459,8 +459,8 @@ and collect_cases = function
 
 let collect_function f =
   collect_type f.fn_return;
-  coqlist_iter (fun (Coq_pair(id, ty)) -> collect_type ty) f.fn_params;
-  coqlist_iter (fun (Coq_pair(id, ty)) -> collect_type ty) f.fn_vars;
+  List.iter (fun (Coq_pair(id, ty)) -> collect_type ty) f.fn_params;
+  List.iter (fun (Coq_pair(id, ty)) -> collect_type ty) f.fn_vars;
   collect_stmt f.fn_body
 
 let collect_fundef (Coq_pair(id, fd)) =
@@ -472,8 +472,8 @@ let collect_globvar (Coq_pair(Coq_pair(id, init), ty)) =
   collect_type ty
 
 let collect_program p =
-  coqlist_iter collect_globvar p.prog_vars;
-  coqlist_iter collect_fundef p.prog_funct
+  List.iter collect_globvar p.prog_vars;
+  List.iter collect_fundef p.prog_funct
 
 let declare_struct_or_union p (name, fld) =
   fprintf p "%s;@ @ " name
@@ -494,8 +494,8 @@ let print_program p prog =
   fprintf p "@[<v 0>";
   StructUnionSet.iter (declare_struct_or_union p) !struct_unions;
   StructUnionSet.iter (print_struct_or_union p) !struct_unions;
-  coqlist_iter (print_globvar p) prog.prog_vars;
-  coqlist_iter (print_fundef p) prog.prog_funct;
+  List.iter (print_globvar p) prog.prog_vars;
+  List.iter (print_fundef p) prog.prog_funct;
   fprintf p "@]@."
 
 
diff --git a/caml/PrintPPC.ml b/caml/PrintPPC.ml
index f4f29402..94c3a7b3 100644
--- a/caml/PrintPPC.ml
+++ b/caml/PrintPPC.ml
@@ -354,10 +354,10 @@ let print_instruction oc labels = function
       if Labelset.mem lbl labels then fprintf oc "%a:\n" print_label lbl
 
 let rec labels_of_code = function
-  | Coq_nil -> Labelset.empty
-  | Coq_cons((Pb lbl | Pbf(_, lbl) | Pbt(_, lbl)), c) ->
+  | [] -> Labelset.empty
+  | (Pb lbl | Pbf(_, lbl) | Pbt(_, lbl)) :: c ->
       Labelset.add lbl (labels_of_code c)
-  | Coq_cons(_, c) -> labels_of_code c
+  | _ :: c -> labels_of_code c
 
 let print_function oc name code =
   Hashtbl.clear current_function_labels;
@@ -365,7 +365,7 @@ let print_function oc name code =
   fprintf oc "	.align 2\n";
   fprintf oc "	.globl %a\n" print_symb name;
   fprintf oc "%a:\n" print_symb name;
-  coqlist_iter (print_instruction oc (labels_of_code code)) code
+  List.iter (print_instruction oc (labels_of_code code)) code
 
 (* Generation of stub code for variadic functions, e.g. printf.
    Calling conventions for variadic functions are:
@@ -401,14 +401,14 @@ let variadic_stub oc stub_name fun_name ty_args =
      As an optimization, don't copy parameters that are already in
      integer registers, since these stay in place. *)
   let rec copy gpr fpr src_ofs dst_ofs = function
-    | Coq_nil -> ()
-    | Coq_cons(Tint, rem) ->
+    | [] -> ()
+    | Tint :: rem ->
         if gpr > 10 then begin
           fprintf oc "	lwz	r0, %d(r1)\n" src_ofs;
           fprintf oc "	stw	r0, %d(r1)\n" dst_ofs
         end;
         copy (gpr + 1) fpr (src_ofs + 4) (dst_ofs + 4) rem
-    | Coq_cons(Tfloat, rem) ->
+    | Tfloat :: rem ->
         if fpr <= 10 then begin
           fprintf oc "	stfd	f%d, %d(r1)\n" fpr dst_ofs
         end else begin
@@ -421,10 +421,10 @@ let variadic_stub oc stub_name fun_name ty_args =
      As an optimization, don't load parameters that are already
      in the correct integer registers. *)
   let rec load gpr ofs = function
-    | Coq_nil -> ()
-    | Coq_cons(Tint, rem) ->
+    | [] -> ()
+    | Tint :: rem ->
         load (gpr + 1) (ofs + 4) rem
-    | Coq_cons(Tfloat, rem) ->
+    | Tfloat :: rem ->
         if gpr <= 10 then
           fprintf oc "	lwz	r%d, %d(r1)\n" gpr ofs;
         if gpr + 1 <= 10 then
@@ -503,20 +503,20 @@ let print_init oc = function
 
 let print_init_data oc id =
   init_data_queue := [];
-  coqlist_iter (print_init oc) id;
+  List.iter (print_init oc) id;
   let rec print_remainder () =
     match !init_data_queue with
     | [] -> ()
     | (lbl, id) :: rem ->
         init_data_queue := rem;
         fprintf oc "L%d:\n" lbl;
-        coqlist_iter (print_init oc) id;
+        List.iter (print_init oc) id;
         print_remainder()
   in print_remainder()
 
 let print_var oc (Coq_pair(Coq_pair(name, init_data), _)) =
   match init_data with
-  | Coq_nil -> ()
+  | [] -> ()
   | _  ->
       fprintf oc "	.data\n";
       fprintf oc "	.align	3\n";
@@ -526,7 +526,7 @@ let print_var oc (Coq_pair(Coq_pair(name, init_data), _)) =
 
 let print_program oc p =
   extfuns := IdentSet.empty;
-  coqlist_iter record_extfun p.prog_funct;
-  coqlist_iter (print_var oc) p.prog_vars;
-  coqlist_iter (print_fundef oc) p.prog_funct
+  List.iter record_extfun p.prog_funct;
+  List.iter (print_var oc) p.prog_vars;
+  List.iter (print_fundef oc) p.prog_funct
 
diff --git a/caml/RTLgenaux.ml b/caml/RTLgenaux.ml
index d9203808..4c1fc05c 100644
--- a/caml/RTLgenaux.ml
+++ b/caml/RTLgenaux.ml
@@ -28,8 +28,8 @@ module IntSet = Set.Make(IntOrd)
 
 let normalize_table tbl =
   let rec norm seen = function
-  | CList.Coq_nil -> []
-  | CList.Coq_cons(Datatypes.Coq_pair(key, act), rem) ->
+  | [] -> []
+  | Datatypes.Coq_pair(key, act) :: rem ->
       if IntSet.mem key seen
       then norm seen rem
       else (key, act) :: norm (IntSet.add key seen) rem
diff --git a/caml/RTLtypingaux.ml b/caml/RTLtypingaux.ml
index 6c43227b..ff704ebe 100644
--- a/caml/RTLtypingaux.ml
+++ b/caml/RTLtypingaux.ml
@@ -32,8 +32,8 @@ let set_type r ty =
 
 let rec set_types rl tyl =
   match rl, tyl with
-  | Coq_nil, Coq_nil -> ()
-  | Coq_cons(r1, rs), Coq_cons(ty1, tys) -> set_type r1 ty1; set_types rs tys
+  | [], [] -> ()
+  | r1 :: rs, ty1 :: tys -> set_type r1 ty1; set_types rs tys
   | _, _ -> raise (Type_error "arity mismatch")
 
 (* First pass: process constraints of the form typeof(r) = ty *)
@@ -98,16 +98,16 @@ let type_instr retty (Coq_pair(pc, i)) =
       end
 
 let type_pass1 retty instrs = 
-  coqlist_iter (type_instr retty) instrs
+  List.iter (type_instr retty) instrs
 
 (* Second pass: extract move constraints typeof(r1) = typeof(r2)
    and solve them iteratively *)
 
 let rec extract_moves = function
-  | Coq_nil -> []
-  | Coq_cons(Coq_pair(pc, i), rem) ->
+  | [] -> []
+  | Coq_pair(pc, i) :: rem ->
       match i with
-      | Iop(Omove, Coq_cons(r1, Coq_nil), r2, _) ->
+      | Iop(Omove, [r1], r2, _) ->
           (r1, r2) :: extract_moves rem
       | Iop(Omove, _, _, _) ->
           raise (Type_error "wrong Omove")
diff --git a/extraction/.depend b/extraction/.depend
index 83dc5dcb..a8ae227f 100644
--- a/extraction/.depend
+++ b/extraction/.depend
@@ -59,9 +59,9 @@
 ../caml/PrintPPC.cmx: PPC.cmx Datatypes.cmx ../caml/Camlcoq.cmx CList.cmx \
     AST.cmx ../caml/PrintPPC.cmi 
 ../caml/RTLgenaux.cmo: Switch.cmi Integers.cmi Datatypes.cmi CminorSel.cmi \
-    ../caml/Camlcoq.cmo CList.cmi 
+    ../caml/Camlcoq.cmo 
 ../caml/RTLgenaux.cmx: Switch.cmx Integers.cmx Datatypes.cmx CminorSel.cmx \
-    ../caml/Camlcoq.cmx CList.cmx 
+    ../caml/Camlcoq.cmx 
 ../caml/RTLtypingaux.cmo: Registers.cmi RTL.cmi Op.cmi Maps.cmi Datatypes.cmi \
     ../caml/Camlcoq.cmo CList.cmi AST.cmi 
 ../caml/RTLtypingaux.cmx: Registers.cmx RTL.cmx Op.cmx Maps.cmx Datatypes.cmx \
diff --git a/extraction/extraction.v b/extraction/extraction.v
index 69034bc1..cdb1fd63 100644
--- a/extraction/extraction.v
+++ b/extraction/extraction.v
@@ -10,6 +10,7 @@
 (*                                                                     *)
 (* *********************************************************************)
 
+Require List.
 Require Iteration.
 Require Floats.
 Require RTLgen.
@@ -21,6 +22,7 @@ Require Main.
 Extract Inductive unit => "unit" [ "()" ].
 Extract Inductive bool => "bool" [ "true" "false" ].
 Extract Inductive sumbool => "bool" [ "true" "false" ].
+Extract Inductive List.list => "list" [ "[]" "(::)" ].
 
 (* Float *)
 Extract Inlined Constant Floats.float => "float".