Extraction: map Coq pairs to Caml pairs and Coq chars (type ascii) to Caml chars

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

17 files changed, 80 insertions, 102 deletions

diff --git a/arm/PrintAsm.ml b/arm/PrintAsm.ml
index 50b585e..a616cc2 100644
--- a/arm/PrintAsm.ml
+++ b/arm/PrintAsm.ml
@@ -201,7 +201,7 @@ let call_helper oc fn dst arg1 arg2 =
   let moves =
     Parmov.parmove2 (=) (fun _ -> IR14) [arg1; arg2] [IR0; IR1] in
   List.iter
-    (fun (Coq_pair(s, d)) ->
+    (fun (s, d) ->
       fprintf oc "	mov	%a, %a\n" ireg d ireg s)
     moves;
   (* Call the helper function *)
@@ -689,7 +689,7 @@ let print_function oc name fn =
   fprintf oc "	.type	%a, %%function\n" print_symb name;
   fprintf oc "	.size	%a, . - %a\n" print_symb name print_symb name
 
-let print_fundef oc (Coq_pair(name, defn)) =
+let print_fundef oc (name, defn) =
   match defn with
   | Internal code ->
       print_function oc name code
@@ -729,7 +729,7 @@ let rec log2 n =
   assert (n > 0);
   if n = 1 then 0 else 1 + log2 (n lsr 1)
 
-let print_var oc (Coq_pair(name, v)) =
+let print_var oc (name, v) =
   match v.gvar_init with
   | [] -> ()
   | _  ->
diff --git a/backend/CMparser.mly b/backend/CMparser.mly
index 0b48c0f..3df3f54 100644
--- a/backend/CMparser.mly
+++ b/backend/CMparser.mly
@@ -141,7 +141,7 @@ let mkswitch expr (cases, dfl) =
   let rec mktable = function
   | [] -> []
   | (key, exit) :: rem ->
-      Coq_pair(coqint_of_camlint key, exitnum exit) :: mktable rem in
+      (coqint_of_camlint key, exitnum exit) :: mktable rem in
   prepend_seq !convert_accu (Sswitch(c, mktable cases, exitnum dfl))
 
 (***
@@ -166,7 +166,7 @@ let mkmatch_aux expr cases =
     | [] -> assert false
     | [key, action] -> []
     | (key, action) :: rem ->
-        Coq_pair(coqint_of_camlint key, nat_of_camlint n)
+        (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
@@ -324,8 +324,8 @@ global_declarations:
 
 global_declaration:
     VAR STRINGLIT LBRACKET INTLIT RBRACKET
-      { Coq_pair($2, {gvar_info = (); gvar_init = [Init_space(z_of_camlint $4)];
-                      gvar_readonly = false; gvar_volatile = false}) }
+      { ($2, {gvar_info = (); gvar_init = [Init_space(z_of_camlint $4)];
+              gvar_readonly = false; gvar_volatile = false}) }
 ;
 
 proc_list:
@@ -345,14 +345,13 @@ proc:
       { let tmp = !temporaries in
         temporaries := [];
         temp_counter := 0;
-        Coq_pair($1,
-        Internal { fn_sig = $6;
-                   fn_params = List.rev $3;
-                   fn_vars = List.rev (tmp @ $9);
-                   fn_stackspace = $8;
-                   fn_body = $10 }) }
+        ($1, Internal { fn_sig = $6;
+                        fn_params = List.rev $3;
+                        fn_vars = List.rev (tmp @ $9);
+                        fn_stackspace = $8;
+                        fn_body = $10 }) }
   | EXTERN STRINGLIT COLON signature 
-      { Coq_pair($2, External(EF_external($2, $4))) }
+      { ($2, External(EF_external($2, $4))) }
 ;
 
 signature:
diff --git a/backend/CMtypecheck.ml b/backend/CMtypecheck.ml
index 819f269..e3a6f70 100644
--- a/backend/CMtypecheck.ml
+++ b/backend/CMtypecheck.ml
@@ -351,7 +351,7 @@ let type_function id f =
   with Error s ->
     raise (Error (sprintf "In function %s:\n%s" (extern_atom id) s))
 
-let type_fundef (Coq_pair (id, fd)) =
+let type_fundef (id, fd) =
   match fd with
   | Internal f -> type_function id f
   | External ef -> ()
diff --git a/backend/Coloringaux.ml b/backend/Coloringaux.ml
index 34fab90..ab7d141 100644
--- a/backend/Coloringaux.ml
+++ b/backend/Coloringaux.ml
@@ -410,11 +410,11 @@ let build g typenv spillcosts =
       n in
   (* Fill the adjacency set and the adjacency lists; compute the degrees. *)
   SetRegReg.fold
-    (fun (Coq_pair(r1, r2)) () ->
+    (fun (r1, r2) () ->
       addEdge (find_reg_node r1) (find_reg_node r2))
     g.interf_reg_reg ();
   SetRegMreg.fold
-    (fun (Coq_pair(r1, mr2)) () ->
+    (fun (r1, mr2) () ->
       addEdge (find_reg_node r1) (find_mreg_node mr2))
     g.interf_reg_mreg ();
   (* Process the moves and insert them in worklistMoves *)
@@ -427,11 +427,11 @@ let build g typenv spillcosts =
     n2.movelist <- m :: n2.movelist;
     DLinkMove.insert m worklistMoves in
   SetRegReg.fold
-    (fun (Coq_pair(r1, r2)) () ->
+    (fun (r1, r2) () ->
       add_move (find_reg_node r1) (find_reg_node r2))
     g.pref_reg_reg ();
   SetRegMreg.fold
-    (fun (Coq_pair(r1, mr2)) () ->
+    (fun (r1, mr2) () ->
       let r1' = find_reg_node r1 in
       if List.mem mr2 !allocatable_registers then
         add_move r1' (find_mreg_node mr2))
diff --git a/backend/PrintCminor.ml b/backend/PrintCminor.ml
index 6a74506..30884b1 100644
--- a/backend/PrintCminor.ml
+++ b/backend/PrintCminor.ml
@@ -223,7 +223,7 @@ let rec print_stmt p s =
   | Sswitch(e, cases, dfl) ->
       fprintf p "@[<v 2>switch (%a) {" print_expr e;
       List.iter
-        (fun (Coq_pair(n, x)) ->
+        (fun (n, x) ->
            fprintf p "@ case %ld: exit %d;\n" 
                      (camlint_of_coqint n) (camlint_of_nat x))
         cases;
@@ -262,7 +262,7 @@ let print_function p id f =
   print_stmt p f.fn_body;
   fprintf p "@;<0 -2>}@]@ "
 
-let print_fundef p (Coq_pair(id, fd)) =
+let print_fundef p (id, fd) =
   match fd with
   | External ef ->
       () (* Todo? *)
diff --git a/backend/PrintLTL.ml b/backend/PrintLTL.ml
index 3bfd803..94f5af0 100644
--- a/backend/PrintLTL.ml
+++ b/backend/PrintLTL.ml
@@ -103,7 +103,7 @@ let print_function pp f =
     List.sort
       (fun (pc1, _) (pc2, _) -> Pervasives.compare pc2 pc1)
       (List.map
-        (fun (Coq_pair(pc, i)) -> (camlint_of_positive pc, i))
+        (fun (pc, i) -> (camlint_of_positive pc, i))
         (PTree.elements f.fn_code)) in
   print_succ pp f.fn_entrypoint 
     (match instrs with (pc1, _) :: _ -> pc1 | [] -> -1l);
diff --git a/backend/PrintRTL.ml b/backend/PrintRTL.ml
index 620a949..985bd63 100644
--- a/backend/PrintRTL.ml
+++ b/backend/PrintRTL.ml
@@ -96,7 +96,7 @@ let print_function pp f =
     List.sort
       (fun (pc1, _) (pc2, _) -> Pervasives.compare pc2 pc1)
       (List.map
-        (fun (Coq_pair(pc, i)) -> (camlint_of_positive pc, i))
+        (fun (pc, i) -> (camlint_of_positive pc, i))
         (PTree.elements f.fn_code)) in
   print_succ pp f.fn_entrypoint 
     (match instrs with (pc1, _) :: _ -> pc1 | [] -> -1l);
diff --git a/backend/RTLgenaux.ml b/backend/RTLgenaux.ml
index 82cb300..0822587 100644
--- a/backend/RTLgenaux.ml
+++ b/backend/RTLgenaux.ml
@@ -29,7 +29,7 @@ module IntSet = Set.Make(IntOrd)
 let normalize_table tbl =
   let rec norm keys accu = function
   | [] -> (accu, keys)
-  | Datatypes.Coq_pair(key, act) :: rem ->
+  | (key, act) :: rem ->
       if IntSet.mem key keys
       then norm keys accu rem
       else norm (IntSet.add key keys) ((key, act) :: accu) rem
diff --git a/backend/RTLtypingaux.ml b/backend/RTLtypingaux.ml
index 17acbc6..5935605 100644
--- a/backend/RTLtypingaux.ml
+++ b/backend/RTLtypingaux.ml
@@ -39,7 +39,7 @@ let rec set_types rl tyl =
 
 (* First pass: process constraints of the form typeof(r) = ty *)
 
-let type_instr retty (Coq_pair(pc, i)) =
+let type_instr retty (pc, i) =
   match i with
   | Inop(_) ->
       ()
@@ -48,7 +48,7 @@ let type_instr retty (Coq_pair(pc, i)) =
   | Iop(op, args, res, _) ->
       if two_address_op op && List.length args >= 1 && List.hd args <> res
       then raise (Type_error "two-address constraint violation");
-      let (Coq_pair(targs, tres)) = type_of_operation op in
+      let (targs, tres) = type_of_operation op in
       set_types args targs; set_type res tres
   | Iload(chunk, addr, args, dst, _) ->
       set_types args (type_of_addressing addr);
@@ -119,7 +119,7 @@ let type_pass1 retty instrs =
 
 let rec extract_moves = function
   | [] -> []
-  | Coq_pair(pc, i) :: rem ->
+  | (pc, i) :: rem ->
       match i with
       | Iop(Omove, [r1], r2, _) ->
           (r1, r2) :: extract_moves rem
diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml
index 2f50a0e..f35598c 100644
--- a/cfrontend/C2C.ml
+++ b/cfrontend/C2C.ml
@@ -132,9 +132,8 @@ let global_for_string s id =
        :: !init in
   add_char '\000';
   for i = String.length s - 1 downto 0 do add_char s.[i] done;
-  Datatypes.Coq_pair(id,
-                     {gvar_info = typeStringLiteral s; gvar_init = !init;
-                      gvar_readonly = true; gvar_volatile = false})
+  (id, {gvar_info = typeStringLiteral s; gvar_init = !init;
+        gvar_readonly = true; gvar_volatile = false})
 
 let globals_for_strings globs =
   Hashtbl.fold
@@ -151,8 +150,7 @@ let register_special_external name ef targs tres =
 
 let declare_special_externals k =
   Hashtbl.fold
-    (fun name fd k ->
-       Datatypes.Coq_pair(intern_string name, fd) :: k)
+    (fun name fd k -> (intern_string name, fd) :: k)
     special_externals_table k
 
 (** ** Handling of stubs for variadic functions *)
@@ -720,7 +718,7 @@ let convertFundef env fd =
       (fun (id, ty) ->
         if Cutil.is_composite_type env ty then
           unsupported "function parameter of struct or union type";
-        Datatypes.Coq_pair(intern_string id.name, convertTyp env ty))
+        (intern_string id.name, convertTyp env ty))
       fd.fd_params in
   let vars =
     List.map
@@ -729,7 +727,7 @@ let convertFundef env fd =
           unsupported "'static' or 'extern' local variable";
         if init <> None then
           unsupported "initialized local variable";
-        Datatypes.Coq_pair(intern_string id.name, convertTyp env ty))
+        (intern_string id.name, convertTyp env ty))
       fd.fd_locals in
   let body' = convertStmt env fd.fd_body in
   let id' = intern_string fd.fd_name.name in
@@ -739,9 +737,8 @@ let convertFundef env fd =
       a_type = Cutil.fundef_typ fd;
       a_fundef = Some fd };
   Sections.define_function env id' fd.fd_ret;
-  Datatypes.Coq_pair(id',
-                     Internal {fn_return = ret; fn_params = params;
-                               fn_vars = vars; fn_body = body'})
+  (id', Internal {fn_return = ret; fn_params = params;
+                  fn_vars = vars; fn_body = body'})
 
 (** External function declaration *)
 
@@ -758,7 +755,7 @@ let convertFundecl env (sto, id, ty, optinit) =
     if List.mem_assoc id.name builtins.functions
     then EF_builtin(id', sg)
     else EF_external(id', sg) in
-  Datatypes.Coq_pair(id', External(ef, args, res))
+  (id', External(ef, args, res))
 
 (** Initializers *)
 
@@ -810,10 +807,8 @@ let convertGlobvar env (sto, id, ty, optinit) =
   let a = Cutil.attributes_of_type env ty in
   let volatile = List.mem C.AVolatile a in
   let readonly = List.mem C.AConst a && not volatile in
-  Datatypes.Coq_pair(id', 
-                     {gvar_info = ty'; gvar_init = init';
-                      gvar_readonly = readonly;
-                      gvar_volatile = volatile})
+  (id', {gvar_info = ty'; gvar_init = init';
+         gvar_readonly = readonly; gvar_volatile = volatile})
 
 (** Convert a list of global declarations.
   Result is a pair [(funs, vars)] where [funs] are 
diff --git a/cfrontend/PrintClight.ml b/cfrontend/PrintClight.ml
index ad6887c..306224b 100644
--- a/cfrontend/PrintClight.ml
+++ b/cfrontend/PrintClight.ml
@@ -231,17 +231,17 @@ let print_function p id f =
                         f.fn_return);
   fprintf p "@[<v 2>{@ ";
   List.iter
-    (fun (Coq_pair(id, ty)) ->
+    (fun (id, ty) ->
       fprintf p "%s;@ " (name_cdecl (extern_atom id) ty))
     f.fn_vars;
   List.iter
-    (fun (Coq_pair(id, ty)) ->
+    (fun (id, ty) ->
       fprintf p "register %s;@ " (name_cdecl (temp_name id) ty))
     f.fn_temps;
   print_stmt p f.fn_body;
   fprintf p "@;<0 -2>}@]@ @ "
 
-let print_fundef p (Coq_pair(id, fd)) =
+let print_fundef p (id, fd) =
   match fd with
   | External(_, args, res) ->
       fprintf p "extern %s;@ @ "
@@ -314,17 +314,17 @@ and collect_cases = function
 
 let collect_function f =
   collect_type f.fn_return;
-  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;
-  List.iter (fun (Coq_pair(id, ty)) -> collect_type ty) f.fn_temps;
+  List.iter (fun (id, ty) -> collect_type ty) f.fn_params;
+  List.iter (fun (id, ty) -> collect_type ty) f.fn_vars;
+  List.iter (fun (id, ty) -> collect_type ty) f.fn_temps;
   collect_stmt f.fn_body
 
-let collect_fundef (Coq_pair(id, fd)) =
+let collect_fundef (id, fd) =
   match fd with
   | External(_, args, res) -> collect_type_list args; collect_type res
   | Internal f -> collect_function f
 
-let collect_globvar (Coq_pair(id, v)) =
+let collect_globvar (id, v) =
   collect_type v.gvar_info
 
 let collect_program p =
diff --git a/cfrontend/PrintCsyntax.ml b/cfrontend/PrintCsyntax.ml
index 6358786..f0e9ee5 100644
--- a/cfrontend/PrintCsyntax.ml
+++ b/cfrontend/PrintCsyntax.ml
@@ -312,7 +312,7 @@ let name_function_parameters fun_name params =
   | _ ->
       let rec add_params first = function
       | [] -> ()
-      | Coq_pair(id, ty) :: rem ->
+      | (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
@@ -328,13 +328,13 @@ let print_function p id f =
                         f.fn_return);
   fprintf p "@[<v 2>{@ ";
   List.iter
-    (fun (Coq_pair(id, ty)) ->
+    (fun (id, ty) ->
       fprintf p "%s;@ " (name_cdecl (extern_atom id) ty))
     f.fn_vars;
   print_stmt p f.fn_body;
   fprintf p "@;<0 -2>}@]@ @ "
 
-let print_fundef p (Coq_pair(id, fd)) =
+let print_fundef p (id, fd) =
   match fd with
   | External(_, args, res) ->
       fprintf p "extern %s;@ @ "
@@ -374,7 +374,7 @@ let print_init p = function
 
 let re_string_literal = Str.regexp "__stringlit_[0-9]+"
 
-let print_globvar p (Coq_pair(id, v)) =
+let print_globvar p (id, v) =
   let name1 = extern_atom id in
   let name2 = if v.gvar_readonly then "const " ^ name1 else name1 in
   let name3 = if v.gvar_volatile then "volatile " ^ name2 else name2 in
@@ -469,16 +469,16 @@ and collect_cases = function
 
 let collect_function f =
   collect_type f.fn_return;
-  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;
+  List.iter (fun (id, ty) -> collect_type ty) f.fn_params;
+  List.iter (fun (id, ty) -> collect_type ty) f.fn_vars;
   collect_stmt f.fn_body
 
-let collect_fundef (Coq_pair(id, fd)) =
+let collect_fundef (id, fd) =
   match fd with
   | External(_, args, res) -> collect_type_list args; collect_type res
   | Internal f -> collect_function f
 
-let collect_globvar (Coq_pair(id, v)) =
+let collect_globvar (id, v) =
   collect_type v.gvar_info
 
 let collect_program p =
diff --git a/driver/Interp.ml b/driver/Interp.ml
index 43f569c..ff097c9 100644
--- a/driver/Interp.ml
+++ b/driver/Interp.ml
@@ -78,7 +78,7 @@ let print_event p = function
 let name_of_fundef prog fd =
   let rec find_name = function
   | [] -> "<unknown function>"
-  | Coq_pair(id, fd') :: rem ->
+  | (id, fd') :: rem ->
       if fd = fd' then extern_atom id else find_name rem
   in find_name prog.prog_funct
 
@@ -131,7 +131,7 @@ let compare_mem m1 m2 =
   if m1 == m2 then 0 else
   let c = compare m1.Mem.nextblock m2.Mem.nextblock in if c <> 0 then c else
   compare_Z_range Z0 m1.Mem.nextblock (fun b ->
-    let (Coq_pair(lo, hi) as bnds) = m1.Mem.bounds b in
+    let ((lo, hi) as bnds) = m1.Mem.bounds b in
     let c = compare bnds (m2.Mem.bounds b) in if c <> 0 then c else
     let contents1 = m1.Mem.mem_contents b and contents2 = m2.Mem.mem_contents b in
     if contents1 == contents2 then 0 else
@@ -328,7 +328,7 @@ let rec world = Determinism.World(world_io, world_vload, world_vstore)
 and world_io id args =
   match chop_stub(extern_atom id), args with
   | "printf", EVptr_global(id, ofs) :: args' ->
-      Some(Coq_pair(EVint Integers.Int.zero, world))
+      Some(EVint Integers.Int.zero, world)
   | _, _ ->
       None
 
@@ -342,7 +342,7 @@ and world_vload chunk id ofs =
     | Mint32 -> EVint(coqint_of_camlint(Random.int32 0x7FFF_FFFFl))
     | Mfloat32 -> EVfloat(Floats.Float.singleoffloat(Random.float 1.0))
     | Mfloat64 -> EVfloat(Random.float 1.0)
-  in Some(Coq_pair(res, world))
+  in Some(res, world)
 
 and world_vstore chunk id ofs v =
   assert !random_volatiles;
@@ -390,7 +390,7 @@ let do_step p prog ge time s =
           fprintf p "@].";
           exit 126
       | l ->
-          List.iter (fun (Coq_pair(t, s')) -> do_events p ge time s t) l;
+          List.iter (fun (t, s') -> do_events p ge time s t) l;
           List.map snd l
 
 let rec explore p prog ge time ss =
@@ -405,14 +405,17 @@ let rec explore p prog ge time ss =
     explore p prog ge (time + 1) ss'
   end
 
+(* Massaging the source program *)
+
 let unvolatile prog =
-  let unvolatile_globvar (Coq_pair(id, gv)) =
-    Coq_pair(id,
-             if gv.gvar_volatile
-             then {gv with gvar_readonly = false; gvar_volatile = false}
-             else gv) in
+  let unvolatile_globvar (id, gv) =
+    (id, if gv.gvar_volatile
+         then {gv with gvar_readonly = false; gvar_volatile = false}
+         else gv) in
   {prog with prog_vars = List.map unvolatile_globvar prog.prog_vars}
 
+(* Execution of a whole program *)
+
 let execute prog =
   Random.self_init();
   let p = err_formatter in
@@ -420,5 +423,5 @@ let execute prog =
   let prog' = if !random_volatiles then prog else unvolatile prog in
   begin match Cexec.do_initial_state prog' with
   | None -> fprintf p "ERROR: Initial state undefined@."
-  | Some(Coq_pair(ge, s)) -> explore p prog ge 0 (StateSet.singleton s)
+  | Some(ge, s) -> explore p prog ge 0 (StateSet.singleton s)
   end
diff --git a/extraction/extraction.v b/extraction/extraction.v
index 4bfac69..52706ab 100644
--- a/extraction/extraction.v
+++ b/extraction/extraction.v
@@ -19,11 +19,8 @@ Require Compiler.
 Require Initializers.
 
 (* Standard lib *)
-Extract Inductive unit => "unit" [ "()" ].
-Extract Inductive bool => "bool" [ "true" "false" ].
-Extract Inductive sumbool => "bool" [ "true" "false" ].
-Extract Inductive option => "option" [ "Some" "None" ].
-Extract Inductive list => "list" [ "[]" "(::)" ].
+Require Import ExtrOcamlBasic.
+Require Import ExtrOcamlString.
 
 (* Float *)
 Extract Inlined Constant Floats.float => "float".
diff --git a/ia32/PrintAsm.ml b/ia32/PrintAsm.ml
index f48b808..5ca56d7 100644
--- a/ia32/PrintAsm.ml
+++ b/ia32/PrintAsm.ml
@@ -114,7 +114,7 @@ let addressing oc (Addrmode(base, shift, cst)) =
   | Coq_inl n ->
       let n = camlint_of_coqint n in
       fprintf oc "%ld" n
-  | Coq_inr(Coq_pair(id, ofs)) -> 
+  | Coq_inr(id, ofs) -> 
       let ofs = camlint_of_coqint ofs in
       if ofs = 0l
       then symbol oc id
@@ -123,8 +123,8 @@ let addressing oc (Addrmode(base, shift, cst)) =
   begin match base, shift with
   | None, None -> ()
   | Some r1, None -> fprintf oc "(%a)" ireg r1
-  | None, Some(Coq_pair(r2,sc)) -> fprintf oc "(,%a,%a)" ireg r2 coqint sc
-  | Some r1, Some(Coq_pair(r2,sc)) -> fprintf oc "(%a,%a,%a)" ireg r1 ireg r2 coqint sc
+  | None, Some(r2,sc) -> fprintf oc "(,%a,%a)" ireg r2 coqint sc
+  | Some r1, Some(r2,sc) -> fprintf oc "(%a,%a,%a)" ireg r1 ireg r2 coqint sc
   end
 
 let name_of_condition = function
@@ -730,7 +730,7 @@ let print_function oc name code =
     jumptables := []
   end
 
-let print_fundef oc (Coq_pair(name, defn)) =
+let print_fundef oc (name, defn) =
   match defn with
   | Internal code -> print_function oc name code
   | External ef -> ()
@@ -761,7 +761,7 @@ let print_init_data oc name id =
   else
     List.iter (print_init oc) id
 
-let print_var oc (Coq_pair(name, v)) =
+let print_var oc (name, v) =
   match v.gvar_init with
   | [] -> ()
   | _  ->
diff --git a/lib/Camlcoq.ml b/lib/Camlcoq.ml
index 34aaa0f..cfbca6e 100644
--- a/lib/Camlcoq.ml
+++ b/lib/Camlcoq.ml
@@ -109,27 +109,11 @@ let extern_atom a =
 
 (* Strings *)
 
-let char_of_ascii (Ascii.Ascii(a0, a1, a2, a3, a4, a5, a6, a7)) =
-  Char.chr(  (if a0 then 1 else 0)
-           + (if a1 then 2 else 0)
-           + (if a2 then 4 else 0)
-           + (if a3 then 8 else 0)
-           + (if a4 then 16 else 0)
-           + (if a5 then 32 else 0)
-           + (if a6 then 64 else 0)
-           + (if a7 then 128 else 0))
-
-let coqstring_length s =
-  let rec len accu = function
-  | String0.EmptyString -> accu
-  | String0.String(_, s) -> len (accu + 1) s
-  in len 0 s
-
-let camlstring_of_coqstring s =
-  let r = String.create (coqstring_length s) in
+let camlstring_of_coqstring (s: char list) =
+  let r = String.create (List.length s) in
   let rec fill pos = function
-  | String0.EmptyString -> r
-  | String0.String(c, s) -> r.[pos] <- char_of_ascii c; fill (pos + 1) s
+  | [] -> r
+  | c :: s -> r.[pos] <- c; fill (pos + 1) s
   in fill 0 s
 
 (* Timing facility *)
diff --git a/powerpc/PrintAsm.ml b/powerpc/PrintAsm.ml
index 3b90ada..91dd686 100644
--- a/powerpc/PrintAsm.ml
+++ b/powerpc/PrintAsm.ml
@@ -920,7 +920,7 @@ let stub_function =
   | MacOS       -> Stubs_MacOS.stub_function
   | Linux|Diab  -> Stubs_EABI.stub_function
 
-let print_fundef oc (Coq_pair(name, defn)) =
+let print_fundef oc (name, defn) =
   match defn with
   | Internal code ->
       print_function oc name code
@@ -929,7 +929,7 @@ let print_fundef oc (Coq_pair(name, defn)) =
   | External _ ->
       ()
 
-let record_extfun (Coq_pair(name, defn)) =
+let record_extfun (name, defn) =
   match defn with
   | Internal _ -> ()
   | External (EF_external _) ->
@@ -967,7 +967,7 @@ let print_init_data oc name id =
   else
     List.iter (print_init oc) id
 
-let print_var oc (Coq_pair(name, v)) =
+let print_var oc (name, v) =
   match v.gvar_init with
   | [] -> ()
   | _  ->