Conflict between extraction/CList and cil/obj/xxx/clist on case-insensitive file systems. Replaced CList by CoqList and likewise for CString and CInt. Removed useless references to CList in hand-written Caml code.

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

11 files changed, 25 insertions, 34 deletions

diff --git a/arm/PrintAsm.ml b/arm/PrintAsm.ml
index 16f22d6..f51a15b 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 f369f9e..c83a46e 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 c4f45b2..819f269 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 d2d2f24..3fdc56f 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 632f2aa..cc7edf4 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 41fe1d4..e5ef64a 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 bb25339..5513b41 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 d4163bb..ac162db 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 b3d2533..879cfe5 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 98fd79c..3660a10 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 352da05..b75d135 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";