diff --git a/arm/PrintAsm.ml b/arm/PrintAsm.ml
index 16f22d60ddd0c0c891f57a1f3754b70a7da5bc31..f51a15b7e2e77a6b1e6c2ac53b49e21168458a0e 100644
--- a/arm/PrintAsm.ml
+++ b/arm/PrintAsm.ml
@@ -14,7 +14,6 @@
open Printf
open Datatypes
-open CList
open Camlcoq
open AST
open Asm
diff --git a/backend/CMparser.mly b/backend/CMparser.mly
index f369f9eacd1d8195fb5267fe3b26dc56c967c558..c83a46e5bad2acb0e1c7c5b37c2de661ae5203e7 100644
--- a/backend/CMparser.mly
+++ b/backend/CMparser.mly
@@ -15,7 +15,6 @@
%{
open Datatypes
-open CList
open Camlcoq
open BinPos
open BinInt
@@ -313,9 +312,9 @@ let mkmatch expr cases =
prog:
global_declarations proc_list EOF
- { { prog_funct = CList.rev $2;
+ { { prog_funct = List.rev $2;
prog_main = intern_string "main";
- prog_vars = CList.rev $1; } }
+ prog_vars = List.rev $1; } }
;
global_declarations:
@@ -347,8 +346,8 @@ proc:
temp_counter := 0;
Coq_pair($1,
Internal { fn_sig = $6;
- fn_params = CList.rev $3;
- fn_vars = CList.rev (CList.app tmp $9);
+ fn_params = List.rev $3;
+ fn_vars = List.rev (tmp @ $9);
fn_stackspace = $8;
fn_body = $10 }) }
| EXTERN STRINGLIT COLON signature
@@ -383,7 +382,7 @@ stack_declaration:
var_declarations:
/* empty */ { [] }
- | var_declarations var_declaration { CList.app $2 $1 }
+ | var_declarations var_declaration { $2 @ $1 }
;
var_declaration:
diff --git a/backend/CMtypecheck.ml b/backend/CMtypecheck.ml
index c4f45b22120eddbefe9b6ae521e48e6da0903a9a..819f269ea4ea9c7a1c6dbb0650f5f672f5004ae3 100644
--- a/backend/CMtypecheck.ml
+++ b/backend/CMtypecheck.ml
@@ -17,7 +17,6 @@
open Printf
open Datatypes
-open CList
open Camlcoq
open AST
open Integers
diff --git a/backend/Linearizeaux.ml b/backend/Linearizeaux.ml
index d2d2f24add95c3a0b2488cacc58fa562446e384f..3fdc56f2b4c43a1c277ab77403e4f2611dfbaabf 100644
--- a/backend/Linearizeaux.ml
+++ b/backend/Linearizeaux.ml
@@ -15,7 +15,6 @@ open Coqlib
open Datatypes
open LTL
open Lattice
-open CList
open Maps
open Camlcoq
@@ -81,4 +80,4 @@ let enumerate_aux f reach =
emit_block (IntSet.remove npc pending) (pos_of_int npc)
end in
emit_block IntSet.empty f.fn_entrypoint;
- CList.rev !enum
+ List.rev !enum
diff --git a/backend/RTLtypingaux.ml b/backend/RTLtypingaux.ml
index 632f2aa51e272e4ac19f62dbbda507ebe28954b1..cc7edf4917bfd82fdd15120c93cb1dee331297af 100644
--- a/backend/RTLtypingaux.ml
+++ b/backend/RTLtypingaux.ml
@@ -13,7 +13,6 @@
(* Type inference for RTL *)
open Datatypes
-open CList
open Camlcoq
open Maps
open AST
diff --git a/cfrontend/Cil2Csyntax.ml b/cfrontend/Cil2Csyntax.ml
index 41fe1d4fe486ea6013eb86162438470b3b126916..e5ef64aaea593e9e7bb0fd54f5732507ecdaa294 100644
--- a/cfrontend/Cil2Csyntax.ml
+++ b/cfrontend/Cil2Csyntax.ml
@@ -19,7 +19,6 @@ CIL -> CabsCoq translator
**************************************************************************)
open Cil
-open CList
open Camlcoq
open AST
open Csyntax
@@ -866,7 +865,7 @@ let convertInit init =
align al;
cvtInit init
- in cvtInit init; CList.rev !k
+ in cvtInit init; List.rev !k
(** Convert a [Cil.initinfo] into a list of [AST.init_data] *)
diff --git a/cfrontend/PrintCsyntax.ml b/cfrontend/PrintCsyntax.ml
index bb25339afea960dfe12fd46dd90a63679418796e..5513b41d4184713720ae54df448ee630e80047ed 100644
--- a/cfrontend/PrintCsyntax.ml
+++ b/cfrontend/PrintCsyntax.ml
@@ -17,7 +17,6 @@
open Format
open Camlcoq
-open CList
open Datatypes
open AST
open Csyntax
diff --git a/extraction/Makefile b/extraction/Makefile
index d4163bb3b767f91bc32f74bbf82d5e20f3e4d142..ac162db78518801a86de66eb1ff626c81c25d36c 100644
--- a/extraction/Makefile
+++ b/extraction/Makefile
@@ -23,13 +23,13 @@ extraction:
rm -f [:lower:]*.mli [:lower:]*.ml
$(COQEXEC) extraction.v
@echo "Fixing file names..."
- @mv list.ml CList.ml
- @mv list.mli CList.mli
- @mv string.ml CString.ml
- @mv string.mli CString.mli
- @mv int.ml CInt.ml
- @mv int.mli CInt.mli
- @echo "Conversion List -> CList, String -> CString, Int -> CInt..."
+ @mv list.ml CoqList.ml
+ @mv list.mli CoqList.mli
+ @mv string.ml CoqString.ml
+ @mv string.mli CoqString.mli
+ @mv int.ml CoqInt.ml
+ @mv int.mli CoqInt.mli
+ @echo "Conversion List -> CoqList, String -> CoqString, Int -> CoqInt..."
@./convert *.mli *.ml
@echo "Patching files..."
@for i in *.patch; do patch < $$i; done
diff --git a/extraction/convert b/extraction/convert
index b3d253360e37db08d94d569cc834c4013ac5fc5f..879cfe50df4f3ef752c95caceb30480145a9773e 100755
--- a/extraction/convert
+++ b/extraction/convert
@@ -1,9 +1,9 @@
#!/usr/bin/perl -pi
-s/\bList\b/CList/g;
-s/\bString\b/CString/g;
-s/\bInt\.Z_as_Int\b/CInt.Z_as_Int/g;
-s/\bInt\.Int\b/CInt.Int/g;
-s/\bInt\.MoreInt\b/CInt.MoreInt/g;
+s/\bList\b/CoqList/g;
+s/\bString\b/CoqString/g;
+s/\bInt\.Z_as_Int\b/CoqInt.Z_as_Int/g;
+s/\bInt\.Int\b/CoqInt.Int/g;
+s/\bInt\.MoreInt\b/CoqInt.MoreInt/g;
s/^open Int$//;
diff --git a/lib/Camlcoq.ml b/lib/Camlcoq.ml
index 98fd79c8a0ba32942483c8a36f45803195eb54b4..3660a10a1747ff08af1ece36a03c1e4a23be1ac7 100644
--- a/lib/Camlcoq.ml
+++ b/lib/Camlcoq.ml
@@ -13,7 +13,6 @@
(* Library of useful Caml <-> Coq conversions *)
open Datatypes
-open CList
open BinPos
open BinInt
@@ -91,15 +90,15 @@ let char_of_ascii (Ascii.Ascii(a0, a1, a2, a3, a4, a5, a6, a7)) =
let coqstring_length s =
let rec len accu = function
- | CString.EmptyString -> accu
- | CString.CString(_, s) -> len (accu + 1) s
+ | CoqString.EmptyString -> accu
+ | CoqString.CoqString(_, s) -> len (accu + 1) s
in len 0 s
let camlstring_of_coqstring s =
let r = String.create (coqstring_length s) in
let rec fill pos = function
- | CString.EmptyString -> r
- | CString.CString(c, s) -> r.[pos] <- char_of_ascii c; fill (pos + 1) s
+ | CoqString.EmptyString -> r
+ | CoqString.CoqString(c, s) -> r.[pos] <- char_of_ascii c; fill (pos + 1) s
in fill 0 s
(* Timing facility *)
diff --git a/powerpc/PrintAsm.ml b/powerpc/PrintAsm.ml
index 352da05ab02c1c761ac8417d0340325b4125ec82..b75d135c30ff617117cfaed061b922b1bc372693 100644
--- a/powerpc/PrintAsm.ml
+++ b/powerpc/PrintAsm.ml
@@ -14,7 +14,6 @@
open Printf
open Datatypes
-open CList
open Camlcoq
open AST
open Asm
@@ -461,9 +460,9 @@ module Stubs_MacOS = struct
let variadic_stub oc stub_name fun_name ty_args =
(* Compute total size of arguments *)
let arg_size =
- CList.fold_left
+ List.fold_left
(fun sz ty -> match ty with Tint -> sz + 4 | Tfloat -> sz + 8)
- ty_args 0 in
+ 0 ty_args in
(* Stack size is linkage area + argument size, with a minimum of 56 bytes *)
let frame_size = max 56 (24 + arg_size) in
fprintf oc " mflr r0\n";