Deactivate warning 27 and added back removed code.

The code was mostly there for documentation effort. So warning
27 is deactivated again.
Bug 18349

47 files changed, 449 insertions, 447 deletions

diff --git a/Makefile.extr b/Makefile.extr
index 324feea9..503c6a6a 100644
--- a/Makefile.extr
+++ b/Makefile.extr
@@ -38,7 +38,7 @@ INCLUDES=$(patsubst %,-I %, $(DIRS))
 # warning 3 = deprecated feature.  Turned off for OCaml 4.02 (bytes vs strings)
 # warning 20 = unused function argument.  There are some in extracted code
 
-WARNINGS=-w +a-4-9-29 -strict-sequence -safe-string -warn-error +a
+WARNINGS=-w +a-4-9-27-29 -strict-sequence -safe-string -warn-error +a
 extraction/%.cmx: WARNINGS +=-w -20-27-32..34-39-41-44..45
 extraction/%.cmo: WARNINGS +=-w -20-27-32..34-39-41-44..45
 
diff --git a/arm/AsmToJSON.ml b/arm/AsmToJSON.ml
index c895bfb2..bb0c0c04 100644
--- a/arm/AsmToJSON.ml
+++ b/arm/AsmToJSON.ml
@@ -14,4 +14,5 @@
 
 (* Dummy function *)
 
-let p_program _ _ = ()
+let p_program oc prog =
+  ()
diff --git a/arm/Asmexpand.ml b/arm/Asmexpand.ml
index e2b0cb6c..3283bb09 100644
--- a/arm/Asmexpand.ml
+++ b/arm/Asmexpand.ml
@@ -381,7 +381,7 @@ let expand_instruction instr =
      else emit (Pldr (IR13,IR13,SOimm ofs))
   | Pbuiltin (ef,args,res) ->
      begin match ef with
-	   | EF_builtin (name,_) ->
+	   | EF_builtin (name,sg) ->
 	      expand_builtin_inline (camlstring_of_coqstring name) args res
 	   | EF_vload chunk ->
 	      expand_builtin_vload chunk args res
diff --git a/arm/TargetPrinter.ml b/arm/TargetPrinter.ml
index 214e789c..87f1057c 100644
--- a/arm/TargetPrinter.ml
+++ b/arm/TargetPrinter.ml
@@ -690,9 +690,9 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET =
       | Pfsts(r1, r2, n) ->
           fprintf oc "	vstr	%a, [%a, #%a]\n" freg_single r1 ireg r2 coqint n; 1
             (* Pseudo-instructions *)
-      | Pallocframe _ ->
+      | Pallocframe(sz, ofs) ->
          assert false
-      | Pfreeframe _ ->
+      | Pfreeframe(sz, ofs) ->
 	 assert false
       | Plabel lbl ->
           fprintf oc "%a:\n" print_label lbl; 0
@@ -725,15 +725,15 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET =
           end
       | Pbuiltin(ef, args, res) ->
           begin match ef with
-          | EF_annot(txt, _) ->
+          | EF_annot(txt, targs) ->
               fprintf oc "%s annotation: " comment;
               print_annot_text preg "sp" oc (camlstring_of_coqstring txt) args;
               0
-          | EF_debug(kind, txt, _) ->
+          | EF_debug(kind, txt, targs) ->
               print_debug_info comment print_file_line preg "sp" oc
                                (P.to_int kind) (extern_atom txt) args;
               0
-          | EF_inline_asm(txt, sg, _) ->
+          | EF_inline_asm(txt, sg, clob) ->
               fprintf oc "%s begin inline assembly\n\t" comment;
               print_inline_asm preg oc (camlstring_of_coqstring txt) sg args res;
               fprintf oc "%s end inline assembly\n" comment;
diff --git a/backend/CMparser.mly b/backend/CMparser.mly
index b20dea38..5109749d 100644
--- a/backend/CMparser.mly
+++ b/backend/CMparser.mly
@@ -210,17 +210,17 @@ let mkmatch_aux expr cases =
   let ncases = List.length cases in
   let rec mktable n = function
     | [] -> assert false
-    | [_, _] -> []
-    | (key, _) :: rem ->
+    | [key, action] -> []
+    | (key, action) :: rem ->
         (coqint_of_camlint key, Nat.of_int n)
         :: mktable (n + 1) rem in
   let sw =
     Sswitch(false, expr, mktable 0 cases, Nat.of_int (ncases - 1)) in
   let rec mkblocks body n = function
     | [] -> assert false
-    | [_, action] ->
+    | [key, action] ->
         Sblock(Sseq(body, action))
-    | (_, action) :: rem ->
+    | (key, action) :: rem ->
         mkblocks
           (Sblock(Sseq(body, Sseq(action, Sexit (Nat.of_int n)))))
           (n - 1)
@@ -233,7 +233,7 @@ let mkmatch expr cases =
   let s =
     match cases with
     | [] -> Sskip (* ??? *)
-    | [_, action] -> action
+    | [key, action] -> action
     | _ -> mkmatch_aux c cases in
   prepend_seq !convert_accu s
 
diff --git a/backend/CMtypecheck.ml b/backend/CMtypecheck.ml
index 399eb9bd..cd0d25dc 100644
--- a/backend/CMtypecheck.ml
+++ b/backend/CMtypecheck.ml
@@ -296,12 +296,12 @@ let rec type_stmt env blk ret s =
   | Sexit n ->
       if Nat.to_int n >= blk then
         raise (Error (sprintf "Bad exit(%d)\n" (Nat.to_int n)))
-  | Sswitch(islong, e, _, _) ->
+  | Sswitch(islong, e, cases, deflt) ->
       unify (type_expr env [] e) (if islong then tlong else tint)
   | Sreturn None ->
       begin match ret with
       | None -> ()
-      | Some _ -> raise (Error ("return without argument"))
+      | Some tret -> raise (Error ("return without argument"))
       end
   | Sreturn (Some e) ->
       begin match ret with
@@ -322,9 +322,9 @@ let rec type_stmt env blk ret s =
       with Error s ->
         raise (Error (sprintf "In tail call:\n%s" s))
       end
-  | Slabel(_, s1) ->
+  | Slabel(lbl, s1) ->
       type_stmt env blk ret s1
-  | Sgoto _ ->
+  | Sgoto lbl ->
       ()
 
 let rec env_of_vars idl =
@@ -343,8 +343,8 @@ let type_function id f =
 let type_globdef (id, gd) =
   match gd with
   | Gfun(Internal f) -> type_function id f
-  | Gfun(External _) -> ()
-  | Gvar _ -> ()
+  | Gfun(External ef) -> ()
+  | Gvar v -> ()
 
 let type_program p =
   List.iter type_globdef p.prog_defs; p
diff --git a/backend/Fileinfo.ml b/backend/Fileinfo.ml
index a78a24db..0490def0 100644
--- a/backend/Fileinfo.ml
+++ b/backend/Fileinfo.ml
@@ -25,7 +25,7 @@ let reset_filenames () =
 
 let close_filenames () =
   Hashtbl.iter
-    (fun _ (_, fb) ->
+    (fun file (num, fb) ->
        match fb with Some b -> Printlines.close b | None -> ())
     filename_info;
   reset_filenames()
@@ -46,7 +46,7 @@ let print_file oc file =
   try
     Hashtbl.find filename_info file
   with Not_found ->
-    let (filenum, _ as res) = enter_filename file in
+    let (filenum, filebuf as res) = enter_filename file in
     fprintf oc "	.file	%d %S\n" filenum file;
     res
 
diff --git a/backend/IRC.ml b/backend/IRC.ml
index 76f194d2..d542f85e 100644
--- a/backend/IRC.ml
+++ b/backend/IRC.ml
@@ -114,7 +114,7 @@ let name_of_loc = function
 
 let name_of_node n =
   match n.var with
-  | V(r, _) -> sprintf "x%ld" (P.to_int32 r)
+  | V(r, ty) -> sprintf "x%ld" (P.to_int32 r)
   | L l -> name_of_loc l
 
 (* The algorithm manipulates partitions of the nodes and of the moves
@@ -455,7 +455,7 @@ let initialNodePartition g =
 
 let _degreeInvariant _ n =
   let c = ref 0 in
-  iterAdjacent (fun _ -> incr c) n;
+  iterAdjacent (fun n -> incr c) n;
   if !c <> n.degree then
     failwith("degree invariant violated by " ^ name_of_node n)
 
@@ -726,7 +726,7 @@ let selectSpill g =
   (* Find a spillable node of minimal cost *)
   let (n, cost) =
     DLinkNode.fold
-      (fun n (_, best_cost as best) ->
+      (fun n (best_node, best_cost as best) ->
         (* Manual inlining of [spillCost] above plus algebraic simplif *)
         let deg = float n.degree in
         let deg2 = deg *. deg in
@@ -883,7 +883,7 @@ let assign_color g n =
 let location_of_var g v =
   match v with
   | L l -> l
-  | V(_, ty) ->
+  | V(r, ty) ->
       try
         let n = Hashtbl.find g.varTable v in
         let n' = getAlias n in
diff --git a/backend/Inliningaux.ml b/backend/Inliningaux.ml
index 7893da89..265831a5 100644
--- a/backend/Inliningaux.ml
+++ b/backend/Inliningaux.ml
@@ -12,5 +12,5 @@
 
 (* To be considered: heuristics based on size of function? *)
 
-let should_inline (id: AST.ident) (_: RTL.coq_function) =
+let should_inline (id: AST.ident) (f: RTL.coq_function) =
   C2C.atom_is_inline id
diff --git a/backend/Linearizeaux.ml b/backend/Linearizeaux.ml
index 41a98873..46d5c3f1 100644
--- a/backend/Linearizeaux.ml
+++ b/backend/Linearizeaux.ml
@@ -79,13 +79,13 @@ let basic_blocks f joins =
        let rec do_instr_list = function
        | [] -> assert false
        | Lbranch s :: _ -> next_in_block blk minpc s
-       | Ltailcall _ :: _ -> end_block blk minpc
-       | Lcond (_, _, ifso, ifnot) :: _ ->
+       | Ltailcall (sig0, ros) :: _ -> end_block blk minpc
+       | Lcond (cond, args, ifso, ifnot) :: _ ->
              end_block blk minpc; start_block ifso; start_block ifnot
-       | Ljumptable(_, tbl) :: _ ->
+       | Ljumptable(arg, tbl) :: _ ->
              end_block blk minpc; List.iter start_block tbl
        | Lreturn :: _ -> end_block blk minpc
-       | _ :: b' -> do_instr_list b' in
+       | instr :: b' -> do_instr_list b' in
        do_instr_list b
   (* next_in_block: check if join point and either extend block
      or start block *)
@@ -110,5 +110,5 @@ let flatten_blocks blks =
 
 (* Build the enumeration *)
 
-let enumerate_aux f _ =
+let enumerate_aux f reach =
   flatten_blocks (basic_blocks f (join_points f))
diff --git a/backend/PrintAsm.ml b/backend/PrintAsm.ml
index 6eff7c02..96aa080e 100644
--- a/backend/PrintAsm.ml
+++ b/backend/PrintAsm.ml
@@ -104,7 +104,7 @@ module Printer(Target:TARGET) =
     let print_globdef oc (name,gdef) =
       match gdef with
       | Gfun (Internal code) -> print_function oc name code
-      | Gfun (External _) ->   ()
+      | Gfun (External ef) ->   ()
       | Gvar v -> print_var oc name v
 
     module DwarfTarget: DwarfTypes.DWARF_TARGET =
diff --git a/backend/PrintLTL.ml b/backend/PrintLTL.ml
index ba28b30d..a0a08218 100644
--- a/backend/PrintLTL.ml
+++ b/backend/PrintLTL.ml
@@ -72,9 +72,9 @@ let print_instruction pp succ = function
   | Lstore(chunk, addr, args, src) ->
       fprintf pp "%s[%a] = %a"
          (name_of_chunk chunk) (print_addressing mreg) (addr, args) mreg src
-  | Lcall(_, fn) ->
+  | Lcall(sg, fn) ->
       fprintf pp "call %a" ros fn
-  | Ltailcall(_, fn) ->
+  | Ltailcall(sg, fn) ->
       fprintf pp "tailcall %a" ros fn
   | Lbuiltin(ef, args, res) ->
       fprintf pp "%a = %s(%a)"
diff --git a/backend/PrintMach.ml b/backend/PrintMach.ml
index 07ec6a1a..517f3037 100644
--- a/backend/PrintMach.ml
+++ b/backend/PrintMach.ml
@@ -57,9 +57,9 @@ let print_instruction pp i =
          (name_of_chunk chunk)
          (PrintOp.print_addressing reg) (addr, args)
          reg src
-  | Mcall(_, fn) ->
+  | Mcall(sg, fn) ->
       fprintf pp "\tcall %a\n" ros fn
-  | Mtailcall(_, fn) ->
+  | Mtailcall(sg, fn) ->
       fprintf pp "\ttailcall %a\n" ros fn
   | Mbuiltin(ef, args, res) ->
       fprintf pp "\t%a = %s(%a)\n"
diff --git a/backend/PrintRTL.ml b/backend/PrintRTL.ml
index a22aa422..ba336b0a 100644
--- a/backend/PrintRTL.ml
+++ b/backend/PrintRTL.ml
@@ -61,11 +61,11 @@ let print_instruction pp (pc, i) =
          (PrintOp.print_addressing reg) (addr, args)
          reg src;
       print_succ pp s (pc - 1)
-  | Icall(_, fn, args, res, s) ->
+  | Icall(sg, fn, args, res, s) ->
       fprintf pp "%a = %a(%a)\n"
         reg res ros fn regs args;
       print_succ pp s (pc - 1)
-  | Itailcall(_, fn, args) ->
+  | Itailcall(sg, fn, args) ->
       fprintf pp "tailcall %a(%a)\n"
         ros fn regs args
   | Ibuiltin(ef, args, res, s) ->
diff --git a/backend/PrintXTL.ml b/backend/PrintXTL.ml
index 1bee1e15..31273f97 100644
--- a/backend/PrintXTL.ml
+++ b/backend/PrintXTL.ml
@@ -67,8 +67,8 @@ let ros pp = function
 
 let liveset pp lv =
   fprintf pp "{";
-  VSet.iter (function V(r, _) -> fprintf pp " x%d" (P.to_int r)
-                    | L _ -> ())
+  VSet.iter (function V(r, ty) -> fprintf pp " x%d" (P.to_int r)
+                    | L l -> ())
     lv;
   fprintf pp " }"
 
@@ -93,9 +93,9 @@ let print_instruction pp succ = function
   | Xstore(chunk, addr, args, src) ->
       fprintf pp "%s[%a] = %a"
          (name_of_chunk chunk) (print_addressing var) (addr, args) var src
-  | Xcall(_, fn, args, res) ->
+  | Xcall(sg, fn, args, res) ->
       fprintf pp "%a = call %a(%a)" vars res ros fn vars args
-  | Xtailcall(_, fn, args) ->
+  | Xtailcall(sg, fn, args) ->
       fprintf pp "tailcall %a(%a)" ros fn vars args
   | Xbuiltin(ef, args, res) ->
       fprintf pp "%a = %s(%a)"
diff --git a/backend/RTLgenaux.ml b/backend/RTLgenaux.ml
index fdf41897..e39d3b56 100644
--- a/backend/RTLgenaux.ml
+++ b/backend/RTLgenaux.ml
@@ -26,22 +26,22 @@ open CminorSel
    putting the bigger of the two branches in fall-through position. *)
 
 let rec size_expr = function
-  | Evar _ -> 0
-  | Eop(_, args) -> 1 + size_exprs args
-  | Eload(_, _, args) -> 1 + size_exprs args
+  | Evar id -> 0
+  | Eop(op, args) -> 1 + size_exprs args
+  | Eload(chunk, addr, args) -> 1 + size_exprs args
   | Econdition(ce, e1, e2) ->
       1 + size_condexpr ce + max (size_expr e1) (size_expr e2)
   | Elet(e1, e2) -> size_expr e1 + size_expr e2
-  | Eletvar _ -> 0
-  | Ebuiltin(_, el) -> 2 + size_exprs el
-  | Eexternal(_, _, el) -> 5 + size_exprs el
+  | Eletvar n -> 0
+  | Ebuiltin(ef, el) -> 2 + size_exprs el
+  | Eexternal(id, sg, el) -> 5 + size_exprs el
 
 and size_exprs = function
   | Enil -> 0
   | Econs(e1, el) -> size_expr e1 + size_exprs el
 
 and size_condexpr = function
-  | CEcond(_, args) -> size_exprs args
+  | CEcond(c, args) -> size_exprs args
   | CEcondition(c1, c2, c3) ->
       1 + size_condexpr c1 + size_condexpr c2 + size_condexpr c3
   | CElet(a, c) ->
@@ -52,8 +52,8 @@ let size_exprlist al = List.fold_right (fun a s -> size_expr a + s) al 0
 let size_builtin_args al = size_exprlist (params_of_builtin_args al)
 
 let rec size_exitexpr = function
-  | XEexit _ -> 0
-  | XEjumptable(arg, _) -> 2 + size_expr arg
+  | XEexit n -> 0
+  | XEjumptable(arg, tbl) -> 2 + size_expr arg
   | XEcondition(c1, c2, c3) ->
       1 + size_condexpr c1 + size_exitexpr c2 + size_exitexpr c3
   | XElet(a, c) ->
@@ -61,34 +61,34 @@ let rec size_exitexpr = function
 
 let rec length_exprs = function
   | Enil -> 0
-  | Econs(_, el) -> 1 + length_exprs el
+  | Econs(e1, el) -> 1 + length_exprs el
 
 let size_eos = function
   | Coq_inl e -> size_expr e
-  | Coq_inr _ -> 0
+  | Coq_inr id -> 0
 
 let rec size_stmt = function
   | Sskip -> 0
-  | Sassign(_, a) -> size_expr a
-  | Sstore(_, _, args, src) -> 1 + size_exprs args + size_expr src
-  | Scall(_, _, eos, args) ->
+  | Sassign(id, a) -> size_expr a
+  | Sstore(chunk, addr, args, src) -> 1 + size_exprs args + size_expr src
+  | Scall(optid, sg, eos, args) ->
       3 + size_eos eos + size_exprs args + length_exprs args
-  | Stailcall(_, eos, args) ->
+  | Stailcall(sg, eos, args) ->
       3 + size_eos eos + size_exprs args + length_exprs args
   | Sbuiltin(_, (EF_annot _ | EF_debug _), _) -> 0
-  | Sbuiltin(_, _, args) -> 1 + size_builtin_args args
+  | Sbuiltin(optid, ef, args) -> 1 + size_builtin_args args
   | Sseq(s1, s2) -> size_stmt s1 + size_stmt s2
   | Sifthenelse(ce, s1, s2) ->
       size_condexpr ce + max (size_stmt s1) (size_stmt s2)
   | Sloop s -> 1 + 4 * size_stmt s
   | Sblock s -> size_stmt s
-  | Sexit _ -> 1
+  | Sexit n -> 1
   | Sswitch xe -> size_exitexpr xe
   | Sreturn None -> 2
   | Sreturn (Some arg) -> 2 + size_expr arg
-  | Slabel(_, s) -> size_stmt s
-  | Sgoto _ -> 1
+  | Slabel(lbl, s) -> size_stmt s
+  | Sgoto lbl -> 1
 
-let more_likely (_: condexpr) (ifso: stmt) (ifnot: stmt) =
+let more_likely (c: condexpr) (ifso: stmt) (ifnot: stmt) =
   size_stmt ifso > size_stmt ifnot
 
diff --git a/backend/Regalloc.ml b/backend/Regalloc.ml
index ee35d7a0..e531a34a 100644
--- a/backend/Regalloc.ml
+++ b/backend/Regalloc.ml
@@ -85,8 +85,8 @@ let constrain_reg v c =
 let rec constrain_regs vl cl =
   match vl, cl with
   | [], _ -> []
-  | _ :: _, [] -> vl
-  | _ :: vl', Some mr1 :: cl' -> L(R mr1) :: constrain_regs vl' cl'
+  | v1 :: vl', [] -> vl
+  | v1 :: vl', Some mr1 :: cl' -> L(R mr1) :: constrain_regs vl' cl'
   | v1 :: vl', None :: cl' -> v1 :: constrain_regs vl' cl'
 
 let move v1 v2 k =
@@ -140,8 +140,8 @@ let convert_builtin_res tyenv = function
 
 let rec constrain_builtin_arg a cl =
   match a, cl with
-  | BA _, None :: cl' -> (a, cl')
-  | BA _, Some mr :: cl' -> (BA (L(R mr)), cl')
+  | BA x, None :: cl' -> (a, cl')
+  | BA x, Some mr :: cl' -> (BA (L(R mr)), cl')
   | BA_splitlong(hi, lo), _ ->
       let (hi', cl1) = constrain_builtin_arg hi cl in
       let (lo', cl2) = constrain_builtin_arg lo cl1 in
@@ -158,8 +158,8 @@ let rec constrain_builtin_args al cl =
 
 let rec constrain_builtin_res a cl =
   match a, cl with
-  | BR _, None :: cl' -> (a, cl')
-  | BR _, Some mr :: cl' -> (BR (L(R mr)), cl')
+  | BR x, None :: cl' -> (a, cl')
+  | BR x, Some mr :: cl' -> (BR (L(R mr)), cl')
   | BR_splitlong(hi, lo), _ ->
       let (hi', cl1) = constrain_builtin_res hi cl in
       let (lo', cl2) = constrain_builtin_res lo cl1 in
@@ -262,7 +262,7 @@ let block_of_RTL_instr funsig tyenv = function
 
 let next_pc f =
   PTree.fold
-    (fun npc pc _ -> if P.lt pc npc then npc else P.succ pc)
+    (fun npc pc i -> if P.lt pc npc then npc else P.succ pc)
     f.RTL.fn_code P.one
 
 (* Translate an RTL function to an XTL function *)
@@ -287,7 +287,7 @@ let vset_removelist vl after = List.fold_right VSet.remove vl after
 let vset_addlist vl after = List.fold_right VSet.add vl after
 
 let vset_addros vos after =
-  match vos with Coq_inl v -> VSet.add v after | Coq_inr _ -> after
+  match vos with Coq_inl v -> VSet.add v after | Coq_inr id -> after
 
 let rec vset_addarg a after =
   match a with
@@ -309,31 +309,31 @@ let live_before instr after =
       if VSet.mem dst after || XTL.is_stack_reg src
       then VSet.add src (VSet.remove dst after)
       else after
-  | Xparmove(srcs, dsts, _, _) ->
+  | Xparmove(srcs, dsts, itmp, ftmp) ->
       vset_addlist srcs (vset_removelist dsts after)
-  | Xop(_, args, res) ->
+  | Xop(op, args, res) ->
       if VSet.mem res after
       then vset_addlist args (VSet.remove res after)
       else after
-  | Xload(_, _, args, dst) ->
+  | Xload(chunk, addr, args, dst) ->
       if VSet.mem dst after
       then vset_addlist args (VSet.remove dst after)
       else after
-  | Xstore(_, _, args, src) ->
+  | Xstore(chunk, addr, args, src) ->
       vset_addlist args (VSet.add src after)
-  | Xcall(_, ros, args, res) ->
+  | Xcall(sg, ros, args, res) ->
       vset_addlist args (vset_addros ros (vset_removelist res after))
-  | Xtailcall(_, ros, args) ->
+  | Xtailcall(sg, ros, args) ->
       vset_addlist args (vset_addros ros VSet.empty)
-  | Xbuiltin(EF_debug _, _, res) ->
+  | Xbuiltin(EF_debug _, args, res) ->
       vset_removeres res after
-  | Xbuiltin(_, args, res) ->
+  | Xbuiltin(ef, args, res) ->
       vset_addargs args (vset_removeres res after)
-  | Xbranch _ ->
+  | Xbranch s ->
       after
-  | Xcond(_, args, _, _) ->
+  | Xcond(cond, args, s1, s2) ->
       List.fold_right VSet.add args after
-  | Xjumptable(arg, _) ->
+  | Xjumptable(arg, tbl) ->
       VSet.add arg after
   | Xreturn args ->
       vset_addlist args VSet.empty
@@ -406,11 +406,11 @@ let dce_instr instr after k =
       | ([src], [dst]) -> Xmove(src, dst) :: k
       | (srcs', dsts') -> Xparmove(srcs', dsts', itmp, ftmp) :: k
       end
-  | Xop(_, _, res) ->
+  | Xop(op, args, res) ->
       if VSet.mem res after
       then instr :: k
       else k
-  | Xload(_, _, _, dst) ->
+  | Xload(chunk, addr, args, dst) ->
       if VSet.mem dst after
       then instr :: k
       else k
@@ -452,8 +452,8 @@ let spill_costs f =
 
   let charge amount uses v =
     match v with
-    | L _ -> ()
-    | V(r, _) ->
+    | L l -> ()
+    | V(r, ty) ->
         let st = get_stats r in
         if st.cost < 0 then
           (* the variable must be spilled, don't change its cost *)
@@ -470,12 +470,12 @@ let spill_costs f =
     List.iter (charge amount uses) vl in
 
   let charge_ros amount ros =
-    match ros with Coq_inl v -> charge amount 1 v | Coq_inr _ -> () in
+    match ros with Coq_inl v -> charge amount 1 v | Coq_inr id -> () in
 
   let force_stack_allocation v =
     match v with
-    | L _ -> ()
-    | V(r,_) ->
+    | L l -> ()
+    | V(r, ty) ->
         let st = get_stats r in
         assert (st.cost < max_int);
         st.cost <- (-1) in
@@ -499,15 +499,15 @@ let spill_costs f =
         charge_list 1 1 srcs; charge_list 1 1 dsts;
         charge max_int 0 itmp; charge max_int 0 ftmp
         (* temps must not be spilled *)
-    | Xop(_, args, res) ->
+    | Xop(op, args, res) ->
         charge_list 10 1 args; charge 10 1 res
-    | Xload(_, _, args, dst) ->
+    | Xload(chunk, addr, args, dst) ->
         charge_list 10 1 args; charge 10 1 dst
-    | Xstore(_, _, args, src) ->
+    | Xstore(chunk, addr, args, src) ->
         charge_list 10 1 args; charge 10 1 src
-    | Xcall(_, vos, _, _) ->
+    | Xcall(sg, vos, args, res) ->
         charge_ros 10 vos
-    | Xtailcall(_, vos, _) ->
+    | Xtailcall(sg, vos, args) ->
         charge_ros 10 vos
     | Xbuiltin(ef, args, res) ->
         begin match ef with
@@ -526,11 +526,11 @@ let spill_costs f =
             charge_list 10 1 (params_of_builtin_res res)
         end
     | Xbranch _ -> ()
-    | Xcond(_, args, _, _) ->
+    | Xcond(cond, args, _, _) ->
         charge_list 10 1 args
     | Xjumptable(arg, _) ->
         charge 10 1 arg
-    | Xreturn _ ->
+    | Xreturn optarg ->
         () in
 
   let charge_block blk = List.iter charge_instr blk in
@@ -620,17 +620,17 @@ let add_interfs_instr g instr live =
             (vset_addlist (res :: argl) (VSet.remove res live))
       end;
       add_interfs_destroyed g (VSet.remove res live) (destroyed_by_op op)
-  | Xload(chunk, addr, _, dst) ->
+  | Xload(chunk, addr, args, dst) ->
       add_interfs_def g dst live;
       add_interfs_destroyed g (VSet.remove dst live)
                               (destroyed_by_load chunk addr)
-  | Xstore(chunk, addr, _,_) ->
+  | Xstore(chunk, addr, args, src) ->
       add_interfs_destroyed g live (destroyed_by_store chunk addr)
-  | Xcall(_, _,_, res) ->
+  | Xcall(sg, vos, args, res) ->
       add_interfs_destroyed g (vset_removelist res live) destroyed_at_call
-  | Xtailcall(_, Coq_inl v, _) ->
+  | Xtailcall(sg, Coq_inl v, args) ->
       List.iter (fun r -> IRC.add_interf g (vmreg r) v) int_callee_save_regs
-  | Xtailcall(_, Coq_inr _, _) ->
+  | Xtailcall(sg, Coq_inr id, args) ->
       ()
   | Xbuiltin(ef, args, res) ->
       (* Interferences with live across *)
@@ -644,7 +644,7 @@ let add_interfs_instr g instr live =
       | EF_annot_val _, [BA arg], BR res ->
           (* like a move *)
           IRC.add_pref g arg res
-      | EF_inline_asm(_, _, clob), _, _ ->
+      | EF_inline_asm(txt, sg, clob), _, _ ->
           let vargs = params_of_builtin_args args in
           (* clobbered regs interfere with res and args for GCC compatibility *)
           List.iter (fun c ->
@@ -656,13 +656,13 @@ let add_interfs_instr g instr live =
             clob
       | _ -> ()
       end
-  | Xbranch _ ->
+  | Xbranch s ->
       ()
-  | Xcond(cond, _, _,_) ->
+  | Xcond(cond, args, s1, s2) ->
       add_interfs_destroyed g live (destroyed_by_cond cond)
-  | Xjumptable _ ->
+  | Xjumptable(arg, tbl) ->
       add_interfs_destroyed g live destroyed_by_jumptable
-  | Xreturn _ ->
+  | Xreturn optarg ->
       ()
 
 let rec add_interfs_block g blk live =
@@ -697,7 +697,7 @@ let addlist_tospill alloc vl ts =
   List.fold_right (add_tospill alloc) vl ts
 
 let addros_tospill alloc ros ts =
-  match ros with Coq_inl v -> add_tospill alloc v ts | Coq_inr _ -> ts
+  match ros with Coq_inl v -> add_tospill alloc v ts | Coq_inr s -> ts
 
 let tospill_instr alloc instr ts =
   match instr with
@@ -705,43 +705,43 @@ let tospill_instr alloc instr ts =
       if is_reg alloc src || is_reg alloc dst || alloc src = alloc dst
       then ts
       else VSet.add src (VSet.add dst ts)
-  | Xreload(_, dst) ->
+  | Xreload(src, dst) ->
       if not (is_reg alloc dst) then begin
         printf "Error: %a was spilled\n" PrintXTL.var dst;
         assert false
       end;
       ts
-  | Xspill(src, _) ->
+  | Xspill(src, dst) ->
       if not (is_reg alloc src) then begin
         printf "Error: %a was spilled\n" PrintXTL.var src;
         assert false
       end;
       ts
-  | Xparmove(_, _, itmp, ftmp) ->
+  | Xparmove(srcs, dsts, itmp, ftmp) ->
       assert (is_reg alloc itmp && is_reg alloc ftmp);
       ts
-  | Xop(_, args, res) ->
+  | Xop(op, args, res) ->
       addlist_tospill alloc args (add_tospill alloc res ts)
-  | Xload(_, _, args, dst) ->
+  | Xload(chunk, addr, args, dst) ->
       addlist_tospill alloc args (add_tospill alloc dst ts)
-  | Xstore(_, _, args, src) ->
+  | Xstore(chunk, addr, args, src) ->
       addlist_tospill alloc args (add_tospill alloc src ts)
-  | Xcall(_, vos, _, _) ->
+  | Xcall(sg, vos, args, res) ->
       addros_tospill alloc vos ts
-  | Xtailcall(_, vos, _) ->
+  | Xtailcall(sg, vos, args) ->
       addros_tospill alloc vos ts
   | Xbuiltin((EF_annot _ | EF_debug _), _, _) ->
       ts
-  | Xbuiltin(_, args, res) ->
+  | Xbuiltin(ef, args, res) ->
       addlist_tospill alloc (params_of_builtin_args args)
          (addlist_tospill alloc (params_of_builtin_res res) ts)
-  | Xbranch _ ->
+  | Xbranch s ->
       ts
-  | Xcond(_, args, _, _) ->
+  | Xcond(cond, args, s1, s2) ->
       addlist_tospill alloc args ts
-  | Xjumptable(arg, _) ->
+  | Xjumptable(arg, tbl) ->
       add_tospill alloc arg ts
-  | Xreturn _ ->
+  | Xreturn optarg ->
       ts
 
 let rec tospill_block alloc blk ts =
@@ -767,13 +767,13 @@ let tospill_function f alloc =
 
 let rec find_reg_containing v = function
   | [] -> None
-  | (var, temp, _) :: eqs ->
+  | (var, temp, date) :: eqs ->
       if var = v then Some temp else find_reg_containing v eqs
 
 let add v t eqs = (v, t, 0) :: eqs
 
 let kill x eqs =
-  List.filter (fun (v, t, _) -> v <> x && t <> x) eqs
+  List.filter (fun (v, t, date) -> v <> x && t <> x) eqs
 
 let reload_var tospill eqs v =
   if not (VSet.mem v tospill) then
@@ -860,11 +860,11 @@ let spill_instr tospill eqs instr =
       end else begin
         ([instr], kill dst eqs)
       end
-  | Xreload _ ->
+  | Xreload(src, dst) ->
       assert false
-  | Xspill _ ->
+  | Xspill(src, dst) ->
       assert false
-  | Xparmove(_, dsts, _, _) ->
+  | Xparmove(srcs, dsts, itmp, ftmp) ->
       ([instr], List.fold_right kill dsts eqs)
   | Xop(op, args, res) ->
       begin match is_two_address op args with
@@ -904,22 +904,22 @@ let spill_instr tospill eqs instr =
       let (src', c2, eqs2) = reload_var tospill eqs1 src in
       (c1 @ c2 @ [Xstore(chunk, addr, args', src')], eqs2)
   | Xcall(sg, Coq_inl v, args, res) ->
-      let (v', c1, _) = reload_var tospill eqs v in
+      let (v', c1, eqs1) = reload_var tospill eqs v in
       (c1 @ [Xcall(sg, Coq_inl v', args, res)], [])
-  | Xcall _ ->
+  | Xcall(sg, Coq_inr id, args, res) ->
       ([instr], [])
   | Xtailcall(sg, Coq_inl v, args) ->
-      let (v', c1, _) = reload_var tospill eqs v in
+      let (v', c1, eqs1) = reload_var tospill eqs v in
       (c1 @ [Xtailcall(sg, Coq_inl v', args)], [])
-  | Xtailcall _ ->
+  | Xtailcall(sg, Coq_inr id, args) ->
       ([instr], [])
-  | Xbuiltin((EF_annot _ | EF_debug _), _, _) ->
+  | Xbuiltin((EF_annot _ | EF_debug _), args, res) ->
       ([instr], eqs)
   | Xbuiltin(ef, args, res) ->
       let (args', c1, eqs1) = reload_args tospill eqs args in
       let (res', c2, eqs2) = save_res tospill eqs1 res in
       (c1 @ Xbuiltin(ef, args', res') :: c2, eqs2)
-  | Xbranch _ ->
+  | Xbranch s ->
       ([instr], eqs)
   | Xcond(cond, args, s1, s2) ->
      let (args', c1, eqs1) = reload_vars tospill eqs args in
@@ -927,7 +927,7 @@ let spill_instr tospill eqs instr =
   | Xjumptable(arg, tbl) ->
       let (arg', c1, eqs1) = reload_var tospill eqs arg in
       (c1 @ [Xjumptable(arg', tbl)], eqs1)
-  | Xreturn _ ->
+  | Xreturn optarg ->
       ([instr], [])
 
 let rec spill_block tospill pc blk eqs =
@@ -1052,9 +1052,9 @@ let transl_instr alloc instr k =
       LTL.Lload(chunk, addr, mregs_of alloc args, mreg_of alloc dst) :: k
   | Xstore(chunk, addr, args, src) ->
       LTL.Lstore(chunk, addr, mregs_of alloc args, mreg_of alloc src) :: k
-  | Xcall(sg, vos, _, _) ->
+  | Xcall(sg, vos, args, res) ->
       LTL.Lcall(sg, mros_of alloc vos) :: k
-  | Xtailcall(sg, vos, _) ->
+  | Xtailcall(sg, vos, args) ->
       LTL.Ltailcall(sg, mros_of alloc vos) :: []
   | Xbuiltin(ef, args, res) ->
       LTL.Lbuiltin(ef, List.map (AST.map_builtin_arg alloc) args,
@@ -1065,7 +1065,7 @@ let transl_instr alloc instr k =
       LTL.Lcond(cond, mregs_of alloc args, s1, s2) :: []
   | Xjumptable(arg, tbl) ->
       LTL.Ljumptable(mreg_of alloc arg, tbl) :: []
-  | Xreturn _ ->
+  | Xreturn optarg ->
       LTL.Lreturn :: []
 
 let rec transl_block alloc blk =
diff --git a/backend/Splitting.ml b/backend/Splitting.ml
index f09da104..40f09c3d 100644
--- a/backend/Splitting.ml
+++ b/backend/Splitting.ml
@@ -73,7 +73,7 @@ module LRMap = struct
 
   let bot : t = RMap.empty
 
-  let lub_opt_range _ olr1 olr2 =
+  let lub_opt_range r olr1 olr2 =
     match olr1, olr2 with
     | Some lr1, Some lr2 -> unify lr1 lr2; olr1
     | Some _, None -> olr1
diff --git a/backend/XTL.ml b/backend/XTL.ml
index 7ff26171..2ddbc50a 100644
--- a/backend/XTL.ml
+++ b/backend/XTL.ml
@@ -99,11 +99,11 @@ let twin_reg r =
 
 let rec successors_block = function
   | Xbranch s :: _ -> [s]
-  | Xtailcall(_,_,_) :: _ -> []
-  | Xcond(_,_, s1, s2) :: _ -> [s1; s2]
-  | Xjumptable(_, tbl) :: _ -> tbl
+  | Xtailcall(sg, vos, args) :: _ -> []
+  | Xcond(cond, args, s1, s2) :: _ -> [s1; s2]
+  | Xjumptable(arg, tbl) :: _ -> tbl
   | Xreturn  _:: _ -> []
-  | _ :: blk -> successors_block blk
+  | instr :: blk -> successors_block blk
   | [] -> assert false
 
 (**** Type checking for XTL *)
@@ -159,25 +159,25 @@ let type_instr = function
   | Xstore(chunk, addr, args, src) ->
       set_vars_type args (type_of_addressing addr);
       set_var_type src (type_of_chunk chunk)
-  | Xcall(_, Coq_inl v, _, _) ->
+  | Xcall(sg, Coq_inl v, args, res) ->
       set_var_type v Tint
-  | Xcall(_, Coq_inr _, _, _) ->
+  | Xcall(sg, Coq_inr id, args, res) ->
       ()
-  | Xtailcall(_, Coq_inl v, _) ->
+  | Xtailcall(sg, Coq_inl v, args) ->
       set_var_type v Tint
-  | Xtailcall(_, Coq_inr _,_) ->
+  | Xtailcall(sg, Coq_inr id, args) ->
       ()
   | Xbuiltin(ef, args, res) ->
       let sg = ef_sig ef in
       type_builtin_args args sg.sig_args;
       type_builtin_res res (proj_sig_res sg)
-  | Xbranch _ ->
+  | Xbranch s ->
       ()
-  | Xcond(cond, args, _, _) ->
+  | Xcond(cond, args, s1, s2) ->
       set_vars_type args (type_of_condition cond)
-  | Xjumptable(arg, _) ->
+  | Xjumptable(arg, tbl) ->
       set_var_type arg Tint
-  | Xreturn _ ->
+  | Xreturn args ->
       ()
 
 let type_block blk =
diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml
index c3e07995..fb4d9a8c 100644
--- a/cfrontend/C2C.ml
+++ b/cfrontend/C2C.ml
@@ -76,13 +76,13 @@ let atom_sections a =
   with Not_found ->
     []
 
-let atom_is_small_data a _ =
+let atom_is_small_data a ofs =
   try
     (Hashtbl.find decl_atom a).a_access = Sections.Access_near
   with Not_found ->
     false
 
-let atom_is_rel_data a _ =
+let atom_is_rel_data a ofs =
   try
     (Hashtbl.find decl_atom a).a_access = Sections.Access_far
   with Not_found ->
@@ -267,7 +267,7 @@ let stringNum = ref 0   (* number of next global for string literals *)
 let stringTable : (string, AST.ident) Hashtbl.t = Hashtbl.create 47
 let wstringTable : (int64 list, AST.ident) Hashtbl.t = Hashtbl.create 47
 
-let name_for_string_literal _ s =
+let name_for_string_literal env s =
   try
     Hashtbl.find stringTable s
   with Not_found ->
@@ -297,7 +297,7 @@ let global_for_string s id =
   (id, Gvar {gvar_info = typeStringLiteral s; gvar_init = !init;
              gvar_readonly = true; gvar_volatile = false})
 
-let name_for_wide_string_literal _ s =
+let name_for_wide_string_literal env s =
   try
     Hashtbl.find wstringTable s
   with Not_found ->
@@ -401,7 +401,7 @@ let make_builtin_va_arg_by_ref helper ty arg =
           Tpointer(Tvoid, noattr)) in
   Evalof(Ederef(Ecast(call, ty_ptr), ty), ty)
 
-let make_builtin_va_arg _ ty e =
+let make_builtin_va_arg env ty e =
   match ty with
   | Ctypes.Tint _ | Tpointer _ ->
       make_builtin_va_arg_by_val
@@ -472,7 +472,7 @@ let checkFunctionType env tres targs =
     | None -> ()
     | Some l ->
         List.iter
-          (fun (_, ty) ->
+          (fun (id, ty) ->
             if Cutil.is_composite_type env ty then
               unsupported "function parameter of struct or union type (consider adding option -fstruct-passing)")
           l
@@ -481,7 +481,7 @@ let checkFunctionType env tres targs =
     
 let rec convertTyp env t =
   match t with
-  | C.TVoid _ -> Tvoid
+  | C.TVoid a -> Tvoid
   | C.TInt(C.ILongLong, a) ->
       Tlong(Signed, convertAttr a)
   | C.TInt(C.IULongLong, a) ->
@@ -513,13 +513,13 @@ let rec convertTyp env t =
       Tstruct(intern_string id.name, convertAttr a)
   | C.TUnion(id, a) ->
       Tunion(intern_string id.name, convertAttr a)
-  | C.TEnum(_, a) ->
+  | C.TEnum(id, a) ->
       let (sg, sz) = convertIkind Cutil.enum_ikind in
       Tint(sz, sg, convertAttr a)
 
 and convertParams env = function
     | [] -> Tnil
-    | (_, ty) :: rem -> Tcons(convertTyp env ty, convertParams env rem)
+    | (id, ty) :: rem -> Tcons(convertTyp env ty, convertParams env rem)
 
 let rec convertTypArgs env tl el =
   match tl, el with
@@ -527,7 +527,7 @@ let rec convertTypArgs env tl el =
   | [], e1 :: el ->
       Tcons(convertTyp env (Cutil.default_argument_conversion env e1.etyp),
             convertTypArgs env [] el)
-  | (_, t1) :: tl, _ :: el ->
+  | (id, t1) :: tl, e1 :: el ->
       Tcons(convertTyp env t1, convertTypArgs env tl el)
 
 let convertField env f =
@@ -550,8 +550,8 @@ let convertCompositedef env su id attr members =
 
 let rec projFunType env ty =
   match Cutil.unroll env ty with
-  | TFun(res, args, vararg, _) -> Some(res, args, vararg)
-  | TPtr(ty', _) -> projFunType env ty'
+  | TFun(res, args, vararg, attr) -> Some(res, args, vararg)
+  | TPtr(ty', attr) -> projFunType env ty'
   | _ -> None
 
 let string_of_type ty =
@@ -663,7 +663,7 @@ let rec convertExpr env e =
   | C.EConst(C.CWStr s) ->
       let ty = typeWideStringLiteral s in
       Evalof(Evar(name_for_wide_string_literal env s, ty), ty)
-  | C.EConst(C.CEnum(_, i)) ->
+  | C.EConst(C.CEnum(id, i)) ->
       Ctyping.econst_int (convertInt i) Signed
   | C.ESizeof ty1 ->
       Ctyping.esizeof (convertTyp env ty1)
@@ -691,7 +691,7 @@ let rec convertExpr env e =
 
   | C.EBinop((C.Oadd|C.Osub|C.Omul|C.Odiv|C.Omod|C.Oand|C.Oor|C.Oxor|
               C.Oshl|C.Oshr|C.Oeq|C.One|C.Olt|C.Ogt|C.Ole|C.Oge) as op,
-             e1, e2, _) ->
+             e1, e2, tyres) ->
       let op' =
         match op with
         | C.Oadd -> Cop.Oadd
@@ -723,7 +723,7 @@ let rec convertExpr env e =
   | C.EBinop((C.Oadd_assign|C.Osub_assign|C.Omul_assign|C.Odiv_assign|
               C.Omod_assign|C.Oand_assign|C.Oor_assign|C.Oxor_assign|
               C.Oshl_assign|C.Oshr_assign) as op,
-             e1, e2, _) ->
+             e1, e2, tyres) ->
       let op' =
         match op with
         | C.Oadd_assign -> Cop.Oadd
@@ -752,7 +752,7 @@ let rec convertExpr env e =
                                 (convertExpr env e2) (convertExpr env e3))
   | C.ECast(ty1, e1) ->
       ewrap (Ctyping.ecast (convertTyp env ty1) (convertExpr env e1))
-  | C.ECompound _ ->
+  | C.ECompound(ty1, ie) ->
       unsupported "compound literals"; ezero
 
   | C.ECall({edesc = C.EVar {name = "__builtin_debug"}}, args) ->
@@ -807,7 +807,7 @@ let rec convertExpr env e =
             Econs(va_list_ptr(convertExpr env arg), Enil),
             convertTyp env e.etyp)
 
-  | C.ECall({edesc = C.EVar {name = "__builtin_va_arg"}}, [arg1; _]) ->
+  | C.ECall({edesc = C.EVar {name = "__builtin_va_arg"}}, [arg1; arg2]) ->
       make_builtin_va_arg env (convertTyp env e.etyp) (convertExpr env arg1)
 
   | C.ECall({edesc = C.EVar {name = "__builtin_va_end"}}, _) ->
@@ -943,7 +943,7 @@ let rec contains_case s =
   | C.Sif(_,s1,s2) -> contains_case s1; contains_case s2
   | C.Swhile (_,s1)
   | C.Sdowhile (s1,_) -> contains_case s1
-  | C.Sfor (s1,_,s2,s3) ->  contains_case s1; contains_case s2; contains_case s3
+  | C.Sfor (s1,e,s2,s3) ->  contains_case s1; contains_case s2; contains_case s3
   | C.Slabeled(C.Scase _, _) ->
       unsupported "'case' outside of 'switch'"
   | C.Slabeled(_,s) -> contains_case s
@@ -1018,7 +1018,7 @@ let rec convertStmt env s =
       unsupported "nested blocks"; Sskip
   | C.Sdecl _ ->
       unsupported "inner declarations"; Sskip
-  | C.Sasm(_, txt, outputs, inputs, clobber) ->
+  | C.Sasm(attrs, txt, outputs, inputs, clobber) ->
       if not !Clflags.option_finline_asm then
         unsupported "inline 'asm' statement (consider adding option -finline-asm)";
       Sdo (convertAsm s.sloc env txt outputs inputs clobber)
@@ -1089,7 +1089,7 @@ let convertFundef loc env fd =
 
 let re_builtin = Str.regexp "__builtin_"
 
-let convertFundecl env (_, id, ty, _) =
+let convertFundecl env (sto, id, ty, optinit) =
   let (args, res, cconv) =
     match convertTyp env ty with
     | Tfunction(args, res, cconv) -> (args, res, cconv)
@@ -1177,11 +1177,11 @@ let rec convertGlobdecls env res gl =
   | g :: gl' ->
       updateLoc g.gloc;
       match g.gdesc with
-      | C.Gdecl((_, id, ty, _) as d) ->
+      | C.Gdecl((sto, id, ty, optinit) as d) ->
           (* Functions become external declarations.
              Other types become variable declarations. *)
           begin match Cutil.unroll env ty with
-          | TFun(_, targs, _, _) ->
+          | TFun(tres, targs, va, a) ->
               if targs = None then
                 warning ("'" ^ id.name ^ "' is declared without a function prototype");
               convertGlobdecls env (convertFundecl env d :: res) gl'
@@ -1251,13 +1251,13 @@ let cleanupGlobals p =
         if IdentSet.mem fd.fd_name !strong then
           error ("multiple definitions of " ^ fd.fd_name.name);
         strong := IdentSet.add fd.fd_name !strong
-    | C.Gdecl(Storage_extern, id, _, _) ->
+    | C.Gdecl(Storage_extern, id, ty, init) ->
         extern := IdentSet.add id !extern
-    | C.Gdecl(_, id, _, Some _) ->
+    | C.Gdecl(sto, id, ty, Some i) ->
         if IdentSet.mem id !strong then
           error ("multiple definitions of " ^ id.name);
         strong := IdentSet.add id !strong
-    | C.Gdecl(_, id, _, None) ->
+    | C.Gdecl(sto, id, ty, None) ->
         weak := IdentSet.add id !weak
     | _ -> () in
   List.iter classify_def p;
@@ -1268,7 +1268,7 @@ let cleanupGlobals p =
     | g :: gl ->
         updateLoc g.gloc;
         match g.gdesc with
-        | C.Gdecl(sto, id, _, init) ->
+        | C.Gdecl(sto, id, ty, init) ->
             let better_def_exists =
               if sto = Storage_extern then
                 IdentSet.mem id !strong || IdentSet.mem id !weak
@@ -1289,7 +1289,7 @@ let cleanupGlobals p =
 
 let public_globals gl =
   List.fold_left
-    (fun accu (id, _) -> if atom_is_static id then accu else id :: accu)
+    (fun accu (id, g) -> if atom_is_static id then accu else id :: accu)
     [] gl
 
 (** Convert a [C.program] into a [Csyntax.program] *)
diff --git a/cfrontend/PrintClight.ml b/cfrontend/PrintClight.ml
index bcdedd53..b8a2cb8d 100644
--- a/cfrontend/PrintClight.ml
+++ b/cfrontend/PrintClight.ml
@@ -134,11 +134,11 @@ let rec print_stmt p s =
                 (temp_name id)
                 print_expr e1
                 print_expr_list (true, el)
-  | Sbuiltin(None, ef, _, el) ->
+  | Sbuiltin(None, ef, tyargs, el) ->
       fprintf p "@[<hv 2>builtin %s@,(@[<hov 0>%a@]);@]"
                 (name_of_external ef)
                 print_expr_list (true, el)
-  | Sbuiltin(Some id, ef, _, el) ->
+  | Sbuiltin(Some id, ef, tyargs, el) ->
       fprintf p "@[<hv 2>%s =@ builtin %s@,(@[<hov 0>%a@]);@]"
                 (temp_name id)
                 (name_of_external ef)
@@ -223,11 +223,11 @@ and print_stmt_for p s =
                 (temp_name id)
                 print_expr e1
                 print_expr_list (true, el)
-  | Sbuiltin(None, ef, _, el) ->
+  | Sbuiltin(None, ef, tyargs, el) ->
       fprintf p "@[<hv 2>builtin %s@,(@[<hov 0>%a@]);@]"
                 (name_of_external ef)
                 print_expr_list (true, el)
-  | Sbuiltin(Some id, ef, _, el) ->
+  | Sbuiltin(Some id, ef, tyargs, el) ->
       fprintf p "@[<hv 2>%s =@ builtin %s@,(@[<hov 0>%a@]);@]"
                 (temp_name id)
                 (name_of_external ef)
diff --git a/cfrontend/PrintCsyntax.ml b/cfrontend/PrintCsyntax.ml
index e3e04c07..d518d6bb 100644
--- a/cfrontend/PrintCsyntax.ml
+++ b/cfrontend/PrintCsyntax.ml
@@ -99,7 +99,7 @@ let rec name_cdecl id ty =
         | Tfunction _ | Tarray _ -> sprintf "(*%s%s)" (attributes_space a) id
         | _                      -> sprintf "*%s%s" (attributes_space a) id in
       name_cdecl id' t
-  | Tarray(t, n, _) ->
+  | Tarray(t, n, a) ->
       name_cdecl (sprintf "%s[%ld]" id (camlint_of_coqint n)) t
   | Tfunction(args, res, cconv) ->
       let b = Buffer.create 20 in
@@ -170,7 +170,7 @@ let rec precedence = function
 
 let print_pointer_hook
    : (formatter -> Values.block * Integers.Int.int -> unit) ref
-   = ref (fun  _ _ -> ())
+   = ref (fun p (b, ofs) -> ())
 
 let print_typed_value p v ty =
   match v, ty with
@@ -233,7 +233,7 @@ let rec expr p (prec, e) =
                  expr (prec1, a1) (name_binop op) expr (prec2, a2)
   | Ecast(a1, ty) ->
       fprintf p "(%s) %a" (name_type ty) expr (prec', a1)
-  | Eassign(res, Ebuiltin(EF_inline_asm(txt, _, clob), _, args, _), _) ->
+  | Eassign(res, Ebuiltin(EF_inline_asm(txt, sg, clob), _, args, _), _) ->
       extended_asm p txt (Some res) args clob
   | Eassign(a1, a2, _) ->
       fprintf p "%a =@ %a" expr (prec1, a1) expr (prec2, a2)
@@ -259,16 +259,16 @@ let rec expr p (prec, e) =
   | Ebuiltin(EF_annot_val(txt, _), _, args, _) ->
       fprintf p "__builtin_annot_val@[<hov 1>(%S%a)@]"
                 (camlstring_of_coqstring txt) exprlist (false, args)
-  | Ebuiltin(EF_external(id, _), _, args, _) ->
+  | Ebuiltin(EF_external(id, sg), _, args, _) ->
       fprintf p "%s@[<hov 1>(%a)@]" (camlstring_of_coqstring id) exprlist (true, args)
-  | Ebuiltin(EF_inline_asm(txt, _, clob), _, args, _) ->
+  | Ebuiltin(EF_inline_asm(txt, sg, clob), _, args, _) ->
       extended_asm p txt None args clob
   | Ebuiltin(EF_debug(kind,txt,_),_,args,_) ->
       fprintf p "__builtin_debug@[<hov 1>(%d,%S%a)@]"
         (P.to_int kind) (extern_atom txt) exprlist (false,args)
   | Ebuiltin(_, _, args, _) ->
       fprintf p "<unknown builtin>@[<hov 1>(%a)@]" exprlist (true, args)
-  | Eparen(a1, tycast, _) ->
+  | Eparen(a1, tycast, ty) ->
       fprintf p "(%s) %a" (name_type tycast) expr (prec', a1)
   end;
   if prec' < prec then fprintf p ")@]" else fprintf p "@]"
@@ -506,7 +506,7 @@ let print_globdef p (id, gd) =
 
 let struct_or_union = function Struct -> "struct" | Union -> "union"
 
-let declare_composite p (Composite(id, su, _, _)) =
+let declare_composite p (Composite(id, su, m, a)) =
   fprintf p "%s %s;@ " (struct_or_union su) (extern_atom id)
 
 let define_composite p (Composite(id, su, m, a)) =
diff --git a/common/PrintAST.ml b/common/PrintAST.ml
index ad3db667..39481bfb 100644
--- a/common/PrintAST.ml
+++ b/common/PrintAST.ml
@@ -37,18 +37,18 @@ let name_of_chunk = function
   | Many64 -> "any64"
 
 let name_of_external = function
-  | EF_external(name, _) -> sprintf "extern %S" (camlstring_of_coqstring name)
-  | EF_builtin(name, _) -> sprintf "builtin %S" (camlstring_of_coqstring name)
+  | EF_external(name, sg) -> sprintf "extern %S" (camlstring_of_coqstring name)
+  | EF_builtin(name, sg) -> sprintf "builtin %S" (camlstring_of_coqstring name)
   | EF_vload chunk -> sprintf "volatile load %s" (name_of_chunk chunk)
   | EF_vstore chunk -> sprintf "volatile store %s" (name_of_chunk chunk)
   | EF_malloc -> "malloc"
   | EF_free -> "free"
   | EF_memcpy(sz, al) ->
       sprintf "memcpy size %s align %s " (Z.to_string sz) (Z.to_string al)
-  | EF_annot(text, _) -> sprintf "annot %S" (camlstring_of_coqstring text)
-  | EF_annot_val(text, _) ->  sprintf "annot_val %S" (camlstring_of_coqstring text)
-  | EF_inline_asm(text, _, _) -> sprintf "inline_asm %S" (camlstring_of_coqstring text)
-  | EF_debug(kind, text, _) ->
+  | EF_annot(text, targs) -> sprintf "annot %S" (camlstring_of_coqstring text)
+  | EF_annot_val(text, targ) ->  sprintf "annot_val %S" (camlstring_of_coqstring text)
+  | EF_inline_asm(text, sg, clob) -> sprintf "inline_asm %S" (camlstring_of_coqstring text)
+  | EF_debug(kind, text, targs) ->
       sprintf "debug%d %S" (P.to_int kind) (extern_atom text)
 
 let rec print_builtin_arg px oc = function
diff --git a/cparser/Bitfields.ml b/cparser/Bitfields.ml
index 6e325ff2..d55a6d36 100644
--- a/cparser/Bitfields.ml
+++ b/cparser/Bitfields.ml
@@ -513,7 +513,7 @@ let transf_decl env (sto, id, ty, init_opt) =
 
 let transf_stmt env s =
   Transform.stmt
-     ~expr:(fun _ env ctx e -> transf_exp env ctx e)
+     ~expr:(fun loc env ctx e -> transf_exp env ctx e)
      ~decl:transf_decl
      env s
 
diff --git a/cparser/Ceval.ml b/cparser/Ceval.ml
index 7a706da2..c3d7eeeb 100644
--- a/cparser/Ceval.ml
+++ b/cparser/Ceval.ml
@@ -80,10 +80,10 @@ let boolean_value v =
 
 let constant = function
   | CInt(v, ik, _) -> I (normalize_int v ik)
-  | CFloat _ -> raise Notconst
+  | CFloat(v, fk) -> raise Notconst
   | CStr s -> S s
   | CWStr s -> WS s
-  | CEnum(_, v) -> I v
+  | CEnum(id, v) -> I v
 
 let is_signed env ty =
   match unroll env ty with
@@ -101,11 +101,11 @@ let cast env ty_to v =
       if sizeof_ikind ik >= !config.sizeof_ptr
       then v
       else raise Notconst
-  | TPtr _, I n ->
+  | TPtr(ty, _), I n ->
       I (normalize_int n (ptr_t_ikind ()))
-  | TPtr _, (S _ | WS _) ->
+  | TPtr(ty, _), (S _ | WS _) ->
       v
-  | TEnum _, I n ->
+  | TEnum(_, _), I n ->
       I (normalize_int n enum_ikind)
   | _, _ ->
       raise Notconst
diff --git a/cparser/Cleanup.ml b/cparser/Cleanup.ml
index 845232aa..fe674d9b 100644
--- a/cparser/Cleanup.ml
+++ b/cparser/Cleanup.ml
@@ -51,18 +51,18 @@ let rec add_typ = function
   | _ -> ()
 
 and add_vars vl =
-  List.iter (fun (_, ty) -> add_typ ty) vl
+  List.iter (fun (id, ty) -> add_typ ty) vl
 
 let rec add_exp e =
   add_typ e.etyp; (* perhaps not necessary but play it safe *)
   match e.edesc with
-  | EConst (CEnum(id, _)) -> addref id
+  | EConst (CEnum(id, v)) -> addref id
   | EConst _ -> ()
   | ESizeof ty -> add_typ ty
   | EAlignof ty -> add_typ ty
   | EVar id -> addref id
-  | EUnop(_, e1) -> add_exp e1
-  | EBinop(_, e1, e2, _) -> add_exp e1; add_exp e2
+  | EUnop(op, e1) -> add_exp e1
+  | EBinop(op, e1, e2, ty) -> add_exp e1; add_exp e2
   | EConditional(e1, e2, e3) -> add_exp e1; add_exp e2; add_exp e3
   | ECast(ty, e1) -> add_typ ty; add_exp e1
   | ECompound(ty, ie) -> add_typ ty; add_init ie
@@ -74,11 +74,11 @@ and add_init = function
   | Init_struct(id, il) -> addref id; List.iter (fun (_, i) -> add_init i) il
   | Init_union(id, _, i) -> addref id; add_init i
 
-let add_decl (_, _, ty, init) =
+let add_decl (sto, id, ty, init) =
   add_typ ty;
   match init with None -> () | Some i -> add_init i
 
-let add_asm_operand (_, _, e) = add_exp e
+let add_asm_operand (lbl, cstr, e) = add_exp e
 
 let rec add_stmt s =
   match s.sdesc with
@@ -95,12 +95,12 @@ let rec add_stmt s =
   | Slabeled(lbl, s) ->
       begin match lbl with Scase e -> add_exp e | _ -> () end;
       add_stmt s
-  | Sgoto _ -> ()
+  | Sgoto lbl -> ()
   | Sreturn None -> ()
   | Sreturn(Some e) -> add_exp e
   | Sblock sl -> List.iter add_stmt sl
   | Sdecl d -> add_decl d
-  | Sasm(_, _, outputs, inputs, _) ->
+  | Sasm(attr, template, outputs, inputs, flags) ->
       List.iter add_asm_operand outputs;
       List.iter add_asm_operand inputs
 
@@ -114,13 +114,13 @@ let add_field f = add_typ f.fld_typ
 
 let add_enum e =
   List.iter
-    (fun (_, _, opt_e) -> match opt_e with Some e -> add_exp e | None -> ())
+    (fun (id, v, opt_e) -> match opt_e with Some e -> add_exp e | None -> ())
     e
 
 (* Saturate the set of referenced identifiers, starting with externally
    visible global declarations *)
 
-let visible_decl (sto, _, ty, _) =
+let visible_decl (sto, id, ty, init) =
   sto = Storage_default &&
   match ty with TFun _ -> false | _ -> true
 
@@ -150,7 +150,7 @@ let rec add_needed_globdecls accu = function
   | [] -> accu
   | g :: rem ->
       match g.gdesc with
-      | Gdecl((_, id, _, _) as decl) ->
+      | Gdecl((sto, id, ty, init) as decl) ->
           if needed id
           then (add_decl decl; add_needed_globdecls accu rem)
           else add_needed_globdecls (g :: accu) rem
@@ -194,14 +194,14 @@ let rec simpl_globdecls accu = function
   | g :: rem ->
       let need =
         match g.gdesc with
-        | Gdecl((_, id, _, _) as decl) -> visible_decl decl || needed id
+        | Gdecl((sto, id, ty, init) as decl) -> visible_decl decl || needed id
         | Gfundef f -> visible_fundef f || needed f.fd_name
         | Gcompositedecl(_, id, _) -> needed id
-        | Gcompositedef(_, id, _, _) -> needed id
-        | Gtypedef(id, _) -> needed id
+        | Gcompositedef(_, id, _, flds) -> needed id
+        | Gtypedef(id, ty) -> needed id
         | Genumdef(id, _, enu) ->
             needed id || List.exists (fun (id, _, _) -> needed id) enu
-        | Gpragma _ -> true in
+        | Gpragma s -> true in
       if need
       then simpl_globdecls (g :: accu) rem
       else begin remove_unused_debug g.gdesc; simpl_globdecls accu rem end
diff --git a/cparser/Cprint.ml b/cparser/Cprint.ml
index 61441aeb..e80a4c8e 100644
--- a/cparser/Cprint.ml
+++ b/cparser/Cprint.ml
@@ -83,7 +83,7 @@ let const pp = function
           else fprintf pp "\" \"\\x%02Lx\" \"" c)
         l;
       fprintf pp "\""
-  | CEnum(id, _) ->
+  | CEnum(id, v) ->
       ident pp id
 
 let attr_arg pp = function
@@ -343,11 +343,11 @@ and init pp = function
       fprintf pp "@[<hov 1>{";
       List.iter (fun i -> fprintf pp "%a,@ " init i) il;
       fprintf pp "}@]"
-  | Init_struct(_, il) ->
+  | Init_struct(id, il) ->
       fprintf pp "@[<hov 1>{";
-      List.iter (fun (_, i) -> fprintf pp "%a,@ " init i) il;
+      List.iter (fun (fld, i) -> fprintf pp "%a,@ " init i) il;
       fprintf pp "}@]"
-  | Init_union(_, fld, i) ->
+  | Init_union(id, fld, i) ->
       fprintf pp "@[<hov 2>{.%s =@ %a}@]" fld.fld_name init i
 
 let simple_decl pp (id, ty) =
@@ -450,7 +450,7 @@ let rec stmt pp s =
       fprintf pp "return;"
   | Sreturn (Some e) ->
       fprintf pp "return %a;" exp (0, e)
-  | Sblock _ ->
+  | Sblock sl ->
       fprintf pp "@[<v 2>{@ %a@;<0 -2>}@]" stmt_block s
   | Sdecl d ->
       full_decl pp d
@@ -535,7 +535,7 @@ let globdecl pp g =
   | Genumdef(id, attrs, vals) ->
       fprintf pp "@[<v 2>enum%a %a {" attributes attrs ident id;
       List.iter
-        (fun (name, _, opt_e) ->
+        (fun (name, v, opt_e) ->
            fprintf pp "@ %a" ident name;
            begin match opt_e with
            | None -> ()
diff --git a/cparser/Cutil.ml b/cparser/Cutil.ml
index 19f6d29a..1bbb8e98 100644
--- a/cparser/Cutil.ml
+++ b/cparser/Cutil.ml
@@ -73,7 +73,7 @@ let rec find_custom_attributes (names: string list)  (al: attributes) =
 let rec remove_custom_attributes (names: string list)  (al: attributes) =
   match al with
   | [] -> []
-  | Attr(name, _) :: tl when List.mem name names ->
+  | Attr(name, args) :: tl when List.mem name names ->
       remove_custom_attributes names tl
   | a :: tl ->
       a :: remove_custom_attributes names tl
@@ -137,12 +137,12 @@ let rec unroll env t =
 let rec attributes_of_type env t =
   match t with
   | TVoid a -> a
-  | TInt(_, a) -> a
-  | TFloat(_, a) -> a
-  | TPtr(_, a) -> a
-  | TArray(ty, _, a) -> add_attributes a (attributes_of_type env ty)
-  | TFun(_, _,_, a) -> a
-  | TNamed(_, _) -> attributes_of_type env (unroll env t)
+  | TInt(ik, a) -> a
+  | TFloat(fk, a) -> a
+  | TPtr(ty, a) -> a
+  | TArray(ty, sz, a) -> add_attributes a (attributes_of_type env ty)
+  | TFun(ty, params, vararg, a) -> a
+  | TNamed(s, a) -> attributes_of_type env (unroll env t)
   | TStruct(s, a) ->
       let ci = Env.find_struct env s in add_attributes ci.ci_attr a
   | TUnion(s, a) ->
@@ -162,7 +162,7 @@ let rec change_attributes_type env (f: attributes -> attributes) t =
   | TArray(ty, sz, a) ->
       TArray(change_attributes_type env f ty, sz, f a)
   | TFun(ty, params, vararg, a) -> TFun(ty, params, vararg, f a)
-  | TNamed(_, _) ->
+  | TNamed(s, a) ->
       let t1 = unroll env t in
       let t2 = change_attributes_type env f t1 in
       if t2 = t1 then t else t2         (* avoid useless expansion *)
@@ -174,7 +174,7 @@ let remove_attributes_type env attr t =
   change_attributes_type env (fun a -> remove_attributes a attr) t
 
 let erase_attributes_type env t =
-  change_attributes_type env (fun _ -> []) t
+  change_attributes_type env (fun a -> []) t
 
 (* Remove all attributes from type that are not contained in attr *)
 let strip_attributes_type t attr =
@@ -224,7 +224,7 @@ let alignas_attribute al =
   let rec alignas_attr accu = function
   | [] -> accu
   | AAlignas n :: al -> alignas_attr (max n accu) al
-  | _ :: al -> alignas_attr accu al
+  | a :: al -> alignas_attr accu al
   in alignas_attr 0 al
 
 (* Type compatibility *)
@@ -260,14 +260,14 @@ let combine_types mode env t1 t2 =
     | None, _ -> sz2
     | _, None -> sz1
     | Some n1, Some n2 -> if n1 = n2 then Some n2 else raise Incompat
-  and comp_conv (_, ty) =
+  and comp_conv (id, ty) =
     match unroll env ty with
-    | TInt(kind, _) ->
+    | TInt(kind, attr) ->
         begin match kind with
         | IBool | IChar | ISChar | IUChar | IShort | IUShort -> raise Incompat
         | _ -> ()
         end
-    | TFloat(kind, _) ->
+    | TFloat(kind, attr) ->
         begin match kind with
         | FFloat -> raise Incompat
         | _ -> ()
@@ -295,7 +295,7 @@ let combine_types mode env t1 t2 =
           | Some l1, None -> List.iter comp_conv l1; (params1, vararg1)
           | Some l1, Some l2 ->
               if List.length l1 <> List.length l2 then raise Incompat;
-              let comp_param (_, ty1) (id2, ty2) =
+              let comp_param (id1, ty1) (id2, ty2) =
                 (id2, comp AttrIgnoreTop ty1 ty2) in
               (Some(List.map2 comp_param l1 l2), comp_base vararg1 vararg2)
         in
@@ -309,8 +309,8 @@ let combine_types mode env t1 t2 =
         TUnion(comp_base s1 s2, comp_attr m a1 a2)
     | TEnum(s1, a1), TEnum(s2, a2) ->
         TEnum(comp_base s1 s2, comp_attr m a1 a2)
-    | TEnum(s,a1), TInt(_,a2)
-    | TInt(_,a2), TEnum (s,a1) ->
+    | TEnum(s,a1), TInt(enum_ikind,a2)
+    | TInt(enum_ikind,a2), TEnum (s,a1) ->
         TEnum(s,comp_attr m a1 a2)
     | _, _ ->
         raise Incompat
@@ -432,7 +432,7 @@ let alignof_struct_union env members =
         | None -> None
         | Some a -> align_rec (max a al) rem
       end else begin
-        let (_, a, ml') = pack_bitfields ml in
+        let (s, a, ml') = pack_bitfields ml in
         align_rec (max a al) ml'
       end
   in align_rec 1 members
@@ -471,7 +471,7 @@ let rec sizeof env t =
   | TInt(ik, _) -> Some(sizeof_ikind ik)
   | TFloat(fk, _) -> Some(sizeof_fkind fk)
   | TPtr(_, _) -> Some(!config.sizeof_ptr)
-  | TArray(_, None, _) -> None
+  | TArray(ty, None, _) -> None
   | TArray(ty, Some n, _) as t' ->
       begin match sizeof env ty with
       | None -> None
@@ -721,7 +721,7 @@ let pointer_decay env t =
 let unary_conversion env t =
   match unroll env t with
   (* Promotion of small integer types *)
-  | TInt(kind, _) ->
+  | TInt(kind, attr) ->
       begin match kind with
       | IBool | IChar | ISChar | IUChar | IShort | IUShort ->
           TInt(IInt, [])
@@ -729,13 +729,13 @@ let unary_conversion env t =
           TInt(kind, [])
       end
   (* Enums are like signed ints *)
-  | TEnum(_, _) -> TInt(enum_ikind, [])
+  | TEnum(id, attr) -> TInt(enum_ikind, [])
   (* Arrays and functions decay automatically to pointers *)
   | TArray(ty, _, _) -> TPtr(ty, [])
   | TFun _ as ty -> TPtr(ty, [])
   (* Float types and pointer types lose their attributes *)
-  | TFloat(kind, _) -> TFloat(kind, [])
-  | TPtr(ty, _) -> TPtr(ty, [])
+  | TFloat(kind, attr) -> TFloat(kind, [])
+  | TPtr(ty, attr) -> TPtr(ty, [])
   (* Other types should not occur, but in doubt... *)
   | _ -> t
 
@@ -859,7 +859,7 @@ let type_of_constant = function
 
 let rec is_lvalue e =
   match e.edesc with
-  | EVar _ -> true
+  | EVar id -> true
   | EUnop((Oderef | Oarrow _), _) -> true
   | EUnop(Odot _, e') -> is_lvalue e'
   | EBinop(Oindex, _, _, _) -> true
@@ -905,8 +905,8 @@ let is_debug_stmt s =
    Custom attributes can safely be dropped or added. *)
 
 let valid_assignment_attr afrom ato =
-  let (afromstd, _) = List.partition attr_is_standard afrom
-  and (atostd,_) = List.partition attr_is_standard ato in
+  let (afromstd, afromcustom) = List.partition attr_is_standard afrom
+  and (atostd, atocustom) = List.partition attr_is_standard ato in
   incl_attributes afromstd atostd
 
 (* Check that an assignment is allowed *)
@@ -1031,11 +1031,11 @@ let rec default_init env ty =
   match unroll env ty with
   | TInt _ | TEnum _ ->
       Init_single (intconst 0L IInt)
-  | TFloat(_, _) ->
+  | TFloat(fk, _) ->
       Init_single floatconst0
-  | TPtr(_, _) ->
+  | TPtr(ty, _) ->
       Init_single nullconst
-  | TArray(_, _, _) ->
+  | TArray(ty, sz, _) ->
       Init_array []
   | TStruct(id, _) ->
       let rec default_init_fields = function
diff --git a/cparser/Elab.ml b/cparser/Elab.ml
index fb75c687..130f37cd 100644
--- a/cparser/Elab.ml
+++ b/cparser/Elab.ml
@@ -90,7 +90,7 @@ let previous_def fn env arg =
 let redef fn env arg =
   match previous_def fn env arg with
   | None -> false
-  | Some(id, _) -> Env.in_current_scope env id
+  | Some(id, info) -> Env.in_current_scope env id
 
 (* Forward declarations *)
 
@@ -289,8 +289,8 @@ let elab_attr_arg loc env a =
   | VARIABLE s ->
       begin try
         match Env.lookup_ident env s with
-        | (_, II_ident _) ->  AIdent s
-        | (_, II_enum v) -> AInt v
+        | (id, II_ident(sto, ty)) ->  AIdent s
+        | (id, II_enum v) -> AInt v
       with Env.Error _ ->
         AIdent s
       end
@@ -477,7 +477,7 @@ let rec elab_specifier ?(only = false) loc env specifier =
     (* Now the other type specifiers *)
 
     | [Cabs.Tnamed id] ->
-        let (id', _) = wrap Env.lookup_typedef loc env id in
+        let (id', info) = wrap Env.lookup_typedef loc env id in
         simple (TNamed(id', []))
 
     | [Cabs.Tstruct_union(STRUCT, id, optmembers, a)] ->
@@ -702,7 +702,7 @@ and elab_struct_or_union_info kind loc env members attrs =
   (* Check for incomplete types *)
   let rec check_incomplete = function
   | [] -> ()
-  | [ { fld_typ = TArray(_, None, _) } ] when kind = Struct -> ()
+  | [ { fld_typ = TArray(ty_elt, None, _) } ] when kind = Struct -> ()
         (* C99: ty[] allowed as last field of a struct *)
   | fld :: rem ->
       if wrap incomplete_type loc env' fld.fld_typ then
@@ -726,7 +726,7 @@ and elab_struct_or_union only kind loc tag optmembers attrs env =
           Env.lookup_composite env s, s
   in
   match optbinding, optmembers with
-  | Some(tag', _), None
+  | Some(tag', ci), None
     when (not only) || Env.in_current_scope env tag' ->
       (* Reference to an already declared struct or union.
          Special case: if this is an "only" declaration (without variable names)
@@ -808,7 +808,7 @@ and elab_enum only loc tag optmembers attrs env =
     if only then
       fatal_error loc
          "forward declaration of 'enum %s' is not allowed in ISO C" tag;
-      let (tag', _) = wrap Env.lookup_enum loc env tag in (tag', env)
+      let (tag', info) = wrap Env.lookup_enum loc env tag in (tag', env)
   | Some members ->
       if tag <> "" && redef Env.lookup_enum env tag then
         error loc "redefinition of 'enum %s'" tag;
@@ -904,12 +904,12 @@ module I = struct
   let top env name ty = (Ztop(name, ty), default_init env ty)
 
   (* Change the initializer for the current point *)
-  let set (z, _) i' = (z, i')
+  let set (z, i) i' = (z, i')
 
   (* Put the current point back to the top *)
   let rec to_top = function
-    | Ztop _, _ as zi -> zi
-    | Zarray(z, _, _,_, before, _, after), i ->
+    | Ztop(name, ty), i as zi -> zi
+    | Zarray(z, ty, sz, dfl, before, idx, after), i ->
         to_top (z, Init_array (List.rev_append before (i :: after)))
     | Zstruct(z, id, before, fld, after), i ->
         to_top (z, Init_struct(id, List.rev_append before ((fld, i) :: after)))
@@ -921,34 +921,34 @@ module I = struct
 
   (* The type of the current point *)
   let typeof = function
-    | Ztop(_, ty), _ -> ty
-    | Zarray(_, ty, _, _, _, _, _), _ -> ty
-    | Zstruct(_, _, _, fld, _), _ -> fld.fld_typ
-    | Zunion(_, _, fld), _ -> fld.fld_typ
+    | Ztop(name, ty), i -> ty
+    | Zarray(z, ty, sz, dfl, before, idx, after), i -> ty
+    | Zstruct(z, id, before, fld, after), i -> fld.fld_typ
+    | Zunion(z, id, fld), i -> fld.fld_typ
 
   (* The name of the path leading to the current point, for error reporting *)
   let rec zipname = function
-    | Ztop(name, _) -> name
-    | Zarray(z, _, _, _, _, idx, _) ->
+    | Ztop(name, ty) -> name
+    | Zarray(z, ty, sz, dfl, before, idx, after) ->
         sprintf "%s[%Ld]" (zipname z) idx
-    | Zstruct(z, _, _, fld, _) ->
+    | Zstruct(z, id, before, fld, after) ->
         sprintf "%s.%s" (zipname z) fld.fld_name
-    | Zunion(z, _, fld) ->
+    | Zunion(z, id, fld) ->
         sprintf "%s.%s" (zipname z) fld.fld_name
 
-  let name (z, _) = zipname z
+  let name (z, i) = zipname z
 
   (* Auxiliary functions to deal with arrays *)
   let index_below (idx: int64) (sz: int64 option) =
     match sz with None -> true | Some sz -> idx < sz
 
-  let il_head dfl = function [] -> dfl | ih :: _ -> ih
-  let il_tail = function [] -> [] | _ :: il -> il
+  let il_head dfl = function [] -> dfl | i1 :: il -> i1
+  let il_tail = function [] -> [] | i1 :: il -> il
 
   (* Advance the current point to the next point in right-up order.
      Return None if no next point, i.e. we are at top *)
   let rec next = function
-    | Ztop _, _ -> None
+    | Ztop(name, ty), i -> None
     | Zarray(z, ty, sz, dfl, before, idx, after), i ->
         let idx' = Int64.succ idx in
         if index_below idx' sz
@@ -973,11 +973,11 @@ module I = struct
           Some(Zarray(z, ty, sz, dfl, [], 0L, il_tail il), il_head dfl il)
         end
         else None
-    | TStruct _, Init_struct(_, []) ->
+    | TStruct(id, _), Init_struct(id', []) ->
         None
-    | TStruct(id, _), Init_struct(_, (fld1, i1) :: flds) ->
+    | TStruct(id, _), Init_struct(id', (fld1, i1) :: flds) ->
         Some(Zstruct(z, id, [], fld1, flds), i1)
-    | TUnion(id, _), Init_union(_, fld, i) ->
+    | TUnion(id, _), Init_union(id', fld, i) ->
         begin match (Env.find_union env id).ci_members with
         | [] -> None
         | fld1 :: _ ->
@@ -986,7 +986,7 @@ module I = struct
                  then i
                  else default_init env fld1.fld_typ)
         end
-    | (TStruct _ | TUnion _), Init_single _ ->
+    | (TStruct _ | TUnion _), Init_single a ->
         (* This is a previous whole-struct initialization that we
            are going to overwrite.  Revert to the default initializer. *)
         first env (z, default_init env ty)
@@ -1019,7 +1019,7 @@ module I = struct
   let rec member env (z, i as zi) name =
     let ty = typeof zi in
     match unroll env ty, i with
-    | TStruct(id, _), Init_struct(_, flds) ->
+    | TStruct(id, _), Init_struct(id', flds) ->
         let rec find before = function
           | [] -> None
           | (fld, i as f_i) :: after ->
@@ -1028,7 +1028,7 @@ module I = struct
               else
                 find (f_i :: before) after
         in find [] flds
-    | TUnion(id, _), Init_union(_, fld, i) ->
+    | TUnion(id, _), Init_union(id', fld, i) ->
         if fld.fld_name = name then
           Some(Zunion(z, id, fld), i)
         else begin
@@ -1041,7 +1041,7 @@ module I = struct
                   find rem
            in find (Env.find_union env id).ci_members
          end
-    | (TStruct _ | TUnion _), Init_single _ ->
+    | (TStruct _ | TUnion _), Init_single a ->
         member env (z, default_init env ty) name
     | _, _ ->
         None
@@ -1126,7 +1126,7 @@ and elab_item zi item il =
       | CStr _, _ ->
           error loc "initialization of an array of non-char elements with a string literal";
           elab_list zi il false
-      | CWStr s, TInt _ ->
+      | CWStr s, TInt(ik, _) ->
           if not (I.index_below (Int64.of_int(List.length s - 1)) sz) then
             warning loc "initializer string for array of wide chars %s is too long"
                         (I.name zi);
@@ -1229,7 +1229,7 @@ let elab_expr loc env a =
 
   | VARIABLE s ->
       begin match wrap Env.lookup_ident loc env s with
-      | (id, II_ident(_, ty)) ->
+      | (id, II_ident(sto, ty)) ->
           { edesc = EVar id; etyp = ty }
       | (id, II_enum v) ->
           { edesc = EConst(CEnum(id, v)); etyp = TInt(enum_ikind, []) }
@@ -1247,7 +1247,7 @@ let elab_expr loc env a =
         match (unroll env b1.etyp, unroll env b2.etyp) with
         | (TPtr(t, _) | TArray(t, _, _)), (TInt _ | TEnum _) -> t
         | (TInt _ | TEnum _), (TPtr(t, _) | TArray(t, _, _)) -> t
-        | _, _ -> error "incorrect types for array subscripting" in
+        | t1, t2 -> error "incorrect types for array subscripting" in
       { edesc = EBinop(Oindex, b1, b2, TPtr(tres, [])); etyp = tres }
 
   | MEMBEROF(a1, fieldname) ->
@@ -1300,7 +1300,7 @@ let elab_expr loc env a =
   | BUILTIN_VA_ARG (a2, a3) ->
       let ident =
         match wrap Env.lookup_ident loc env "__builtin_va_arg" with
-          | (id, II_ident(_, ty)) -> { edesc = EVar id; etyp = ty }
+          | (id, II_ident(sto, ty)) -> { edesc = EVar id; etyp = ty }
           | _ -> assert false
       in
       let b2 = elab a2 and b3 = elab (TYPE_SIZEOF a3) in
@@ -1329,10 +1329,10 @@ let elab_expr loc env a =
       (* Extract type information *)
       let (res, args, vararg) =
         match unroll env b1.etyp with
-        | TFun(res, args, vararg, _) -> (res, args, vararg)
-        | TPtr(ty, _) ->
+        | TFun(res, args, vararg, a) -> (res, args, vararg)
+        | TPtr(ty, a) ->
             begin match unroll env ty with
-            | TFun(res, args, vararg, _) -> (res, args, vararg)
+            | TFun(res, args, vararg, a) -> (res, args, vararg)
             | _ -> error "the function part of a call does not have a function type"
             end
         | _ -> error "the function part of a call does not have a function type"
@@ -1364,7 +1364,7 @@ let elab_expr loc env a =
       let (ty, _) = elab_type loc env spec dcl in
       begin match elab_initializer loc env "<compound literal>" ty ie with
       | (ty', Some i) -> { edesc = ECompound(ty', i); etyp = ty' }
-      | (_, None)   -> error "ill-formed compound literal"
+      | (ty', None)   -> error "ill-formed compound literal"
       end
 
 (* 6.5.3 Unary expressions *)
@@ -1487,8 +1487,8 @@ let elab_expr loc env a =
         else begin
           let ty =
             match unroll env b1.etyp, unroll env b2.etyp with
-            | (TPtr(ty, _) | TArray(ty, _, _)), (TInt _ | TEnum _) -> ty
-            | (TInt _ | TEnum _), (TPtr(ty, _) | TArray(ty, _, _)) -> ty
+            | (TPtr(ty, a) | TArray(ty, _, a)), (TInt _ | TEnum _) -> ty
+            | (TInt _ | TEnum _), (TPtr(ty, a) | TArray(ty, _, a)) -> ty
             | _, _ -> error "type error in binary '+'" in
           if not (pointer_arithmetic_ok env ty) then
             err "illegal pointer arithmetic in binary '+'";
@@ -1505,16 +1505,16 @@ let elab_expr loc env a =
           (tyres, tyres)
         end else begin
           match unroll env b1.etyp, unroll env b2.etyp with
-          | (TPtr(ty, _) | TArray(ty, _, _)), (TInt _ | TEnum _) ->
+          | (TPtr(ty, a) | TArray(ty, _, a)), (TInt _ | TEnum _) ->
               if not (pointer_arithmetic_ok env ty) then
                 err "illegal pointer arithmetic in binary '-'";
               (TPtr(ty, []), TPtr(ty, []))
-          | (TInt _ | TEnum _), (TPtr(ty, _) | TArray(ty, _, _)) ->
+          | (TInt _ | TEnum _), (TPtr(ty, a) | TArray(ty, _, a)) ->
               if not (pointer_arithmetic_ok env ty) then
                 err "illegal pointer arithmetic in binary '-'";
               (TPtr(ty, []), TPtr(ty, []))
-          | (TPtr(ty1, _) | TArray(ty1, _, _)),
-            (TPtr(ty2, _) | TArray(ty2, _, _)) ->
+          | (TPtr(ty1, a1) | TArray(ty1, _, a1)),
+            (TPtr(ty2, a2) | TArray(ty2, _, a2)) ->
               if not (compatible_types AttrIgnoreAll env ty1 ty2) then
                 err "mismatch between pointer types in binary '-'";
               if not (pointer_arithmetic_ok env ty1) then
@@ -1585,9 +1585,9 @@ let elab_expr loc env a =
               | Some ty -> ty
             in
           { edesc = EConditional(b1, b2, b3); etyp = tyres }
-      | TPtr(ty1, _), TInt _ when is_literal_0 b3 ->
+      | TPtr(ty1, a1), TInt _ when is_literal_0 b3 ->
           { edesc = EConditional(b1, b2, nullconst); etyp = TPtr(ty1, []) }
-      | TInt _, TPtr(ty2, _) when is_literal_0 b2 ->
+      | TInt _, TPtr(ty2, a2) when is_literal_0 b2 ->
           { edesc = EConditional(b1, nullconst, b3); etyp = TPtr(ty2, []) }
       | ty1, ty2 ->
           match combine_types AttrIgnoreAll env ty1 ty2 with
@@ -1795,7 +1795,7 @@ let enter_typedefs loc env sto dl =
     if init <> NO_INIT then
       error loc "initializer in typedef";
     match previous_def Env.lookup_typedef env s with
-    | Some (_ ,ty') ->
+    | Some (s',ty') ->
         if equal_types env ty ty' then begin
           warning loc "redefinition of typedef '%s'" s;
           env
@@ -1846,7 +1846,7 @@ let enter_or_refine_ident local loc env s sto ty =
 	| Storage_register,_ -> Storage_register
       in
       (id, new_sto, Env.add_ident env id new_sto new_ty,new_ty)
-  | Some(id, II_enum _) when Env.in_current_scope env id ->
+  | Some(id, II_enum v) when Env.in_current_scope env id ->
       error loc "redefinition of enumerator '%s'" s;
       (id, sto, Env.add_ident env id sto ty,ty)
   | _ ->
@@ -1913,7 +1913,7 @@ let elab_fundef env spec name defs body loc =
           fatal_error loc "Parameter '%s' appears more than once in function declaration" id)
         params;
       (* Check that the declarations only declare parameters *)
-      let extract_name (Init_name(Name(s, _, _, loc') as name, ie)) =
+      let extract_name (Init_name(Name(s, dty, attrs, loc') as name, ie)) =
         if not (List.mem s params) then
           error loc' "Declaration of '%s' which is not a function parameter" s;
         if ie <> NO_INIT then
@@ -1947,7 +1947,7 @@ let elab_fundef env spec name defs body loc =
       in
       let params' = List.map search_param_type params in
       (TFun(ty_ret, Some params', false, attr), env1)
-    | _, Some _ -> assert false
+    | _, Some params -> assert false
   in
   (* Extract info from type *)
   let (ty_ret, params, vararg, attr) =
@@ -2093,7 +2093,7 @@ let rec elab_stmt env ctx s =
       begin match Ceval.integer_expr env a' with
         | None ->
             error loc "argument of 'case' must be an integer compile-time constant"
-        | Some _ -> ()
+        | Some n -> ()
       end;
       { sdesc = Slabeled(Scase a', elab_stmt env ctx s1); sloc = elab_loc loc }
 
diff --git a/cparser/Env.ml b/cparser/Env.ml
index 9ab5e657..dae79ef2 100644
--- a/cparser/Env.ml
+++ b/cparser/Env.ml
@@ -120,7 +120,7 @@ let lookup_ident env s =
 
 let lookup_struct env s =
   try
-    let (_, ci as res) = IdentMap.lookup s env.env_tag in
+    let (id, ci as res) = IdentMap.lookup s env.env_tag in
     if ci.ci_kind <> Struct then
       raise(Error(Tag_mismatch(s, "struct", "union")));
     res
@@ -129,7 +129,7 @@ let lookup_struct env s =
 
 let lookup_union env s =
   try
-    let (_, ci as res) = IdentMap.lookup s env.env_tag in
+    let (id, ci as res) = IdentMap.lookup s env.env_tag in
     if ci.ci_kind <> Union then
       raise(Error(Tag_mismatch(s, "union", "struct")));
     res
@@ -245,7 +245,7 @@ let add_typedef env id info =
   { env with env_typedef = IdentMap.add id info env.env_typedef }
 
 let add_enum env id info =
-  let add_enum_item env (id, v, _) =
+  let add_enum_item env (id, v, exp) =
     { env with env_ident = IdentMap.add id (II_enum v) env.env_ident } in
   List.fold_left add_enum_item
     { env with env_enum = IdentMap.add id info env.env_enum }
diff --git a/cparser/ExtendedAsm.ml b/cparser/ExtendedAsm.ml
index 5183df9b..c3d80272 100644
--- a/cparser/ExtendedAsm.ml
+++ b/cparser/ExtendedAsm.ml
@@ -150,7 +150,7 @@ let transf_outputs loc env = function
          when substituting the text *)
       let rec bind_outputs pos subst = function
       | [] -> (None, [], subst, pos, pos)
-      | (lbl, _, _) :: outputs ->
+      | (lbl, cstr, e) :: outputs ->
           bind_outputs (pos + 1) (set_label_reg lbl pos pos subst) outputs
       in bind_outputs 0 StringMap.empty outputs
 
diff --git a/cparser/Lexer.mll b/cparser/Lexer.mll
index b2b00e8c..871f2bf9 100644
--- a/cparser/Lexer.mll
+++ b/cparser/Lexer.mll
@@ -577,7 +577,7 @@ and singleline_comment = parse
           let rec doConcat wide str =
             try
               match Queue.peek tokens with
-              | STRING_LITERAL (wide', str', _) ->
+              | STRING_LITERAL (wide', str', loc) ->
                   ignore (Queue.pop tokens);
                   let (wide'', str'') = doConcat wide' str' in
                   if str'' <> []
diff --git a/cparser/PackedStructs.ml b/cparser/PackedStructs.ml
index 6a60dfb8..aafa1caa 100644
--- a/cparser/PackedStructs.ml
+++ b/cparser/PackedStructs.ml
@@ -129,8 +129,8 @@ let transf_composite loc env su id attrs ml =
 
 let lookup_function env name =
   match Env.lookup_ident env name with
-  | (id, II_ident(_, ty)) -> (id, ty)
-  | (_, II_enum _) -> raise (Env.Error(Env.Unbound_identifier name))
+  | (id, II_ident(sto, ty)) -> (id, ty)
+  | (id, II_enum _) -> raise (Env.Error(Env.Unbound_identifier name))
 
 (* Type for the access *)
 
@@ -387,7 +387,7 @@ let rec transf_globdecls env accu = function
   | [] -> List.rev accu
   | g :: gl ->
       match g.gdesc with
-      | Gdecl((sto, id, ty, _) as d) ->
+      | Gdecl((sto, id, ty, init) as d) ->
           transf_globdecls
             (Env.add_ident env id sto ty)
             ({g with gdesc = Gdecl(transf_decl g.gloc env d)} :: accu)
@@ -422,7 +422,7 @@ let rec transf_globdecls env accu = function
             (Env.add_enum env id {ei_members =  el; ei_attr = attr})
             (g :: accu)
             gl
-      | Gpragma _ ->
+      | Gpragma p ->
           transf_globdecls env (g :: accu) gl
 
 (* Program *)
diff --git a/cparser/Rename.ml b/cparser/Rename.ml
index 0d92c514..664f6a28 100644
--- a/cparser/Rename.ml
+++ b/cparser/Rename.ml
@@ -182,7 +182,7 @@ and stmt_desc env = function
   | Sgoto lbl -> Sgoto lbl
   | Sreturn a -> Sreturn (optexp env a)
   | Sblock sl -> let (sl', _) = mmap stmt_or_decl env sl in Sblock sl'
-  | Sdecl _ -> assert false
+  | Sdecl d -> assert false
   | Sasm(attr, txt, outputs, inputs, flags) ->
        Sasm(attr, txt,
             List.map (asm_operand env) outputs,
diff --git a/cparser/StructReturn.ml b/cparser/StructReturn.ml
index 95f133bd..04f0021a 100644
--- a/cparser/StructReturn.ml
+++ b/cparser/StructReturn.ml
@@ -217,7 +217,7 @@ let rec transf_type env t =
           TFun(tres', None, vararg, attr)
       | Ret_ref ->
           TFun(TVoid [], None, vararg, add_attributes attr attr_structret)
-      | Ret_value(ty, _, _) ->
+      | Ret_value(ty, sz, al) ->
           TFun(ty, None, vararg, attr)
       end
   | TFun(tres, Some args, vararg, attr) ->
@@ -230,7 +230,7 @@ let rec transf_type env t =
           let res = Env.fresh_ident "_res" in
           TFun(TVoid [], Some((res, TPtr(tres', [])) :: args'), vararg,
                add_attributes attr attr_structret)
-      | Ret_value(ty, _, _) ->
+      | Ret_value(ty, sz, al) ->
           TFun(ty, Some args', vararg, attr)
       end
   | TPtr(t1, attr) ->
@@ -251,7 +251,7 @@ and transf_funargs env = function
           (id, t') :: args'
       | Param_ref_caller ->
           (id, TPtr(t', [])) :: args'
-      | Param_flattened(n, _, _) ->
+      | Param_flattened(n, sz, al) ->
           list_map_n (fun _ -> (Env.fresh_ident id.name, uint)) n
           @ args'
 
@@ -261,7 +261,7 @@ let rec translates_to_extended_lvalue arg =
   is_lvalue arg ||
   (match arg.edesc with
    | ECall _ -> true
-   | EBinop(Ocomma, _, b, _) -> translates_to_extended_lvalue b
+   | EBinop(Ocomma, a, b, _) -> translates_to_extended_lvalue b
    | _ -> false)
 
 let rec transf_expr env ctx e =
@@ -279,7 +279,7 @@ let rec transf_expr env ctx e =
       {edesc = EUnop(op, transf_expr env Val e1); etyp = newty}
   | EBinop(Oassign, lhs, {edesc = ECall(fn, args); etyp = ty}, _) ->
       transf_call env ctx (Some (transf_expr env Val lhs)) fn args ty
-  | EBinop(Ocomma, e1, e2, _) ->
+  | EBinop(Ocomma, e1, e2, ty) ->
       ecomma (transf_expr env Effects e1) (transf_expr env ctx e2)
   | EBinop(op, e1, e2, ty) ->
       {edesc = EBinop(op, transf_expr env Val e1,
@@ -349,7 +349,7 @@ and transf_call env ctx opt_lhs fn args ty =
               ecomma {edesc = ECall(fn', eaddrof tmp :: args'); etyp = TVoid []}
                      (eassign lhs tmp)
           end
-      | Ret_value(ty_ret, _, _) ->
+      | Ret_value(ty_ret, sz, al) ->
           let ecall = {edesc = ECall(fn', args'); etyp = ty_ret} in
           begin match ctx, opt_lhs with
           | Effects, None ->
@@ -461,7 +461,7 @@ let rec transf_stmt s =
       {s with sdesc = Sswitch(transf_expr Val e, transf_stmt s1)}
   | Slabeled(lbl, s1) ->
       {s with sdesc = Slabeled(lbl, transf_stmt s1)}
-  | Sgoto _ -> s
+  | Sgoto lbl -> s
   | Sreturn None -> s
   | Sreturn(Some e) ->
       let e' = transf_expr Val e in
@@ -524,7 +524,7 @@ let rec transf_funparams loc env params =
           ((x, tpx) :: params',
            actions,
            IdentMap.add x estarx subst)
-      | Param_flattened(n, _, _) ->
+      | Param_flattened(n, sz, al) ->
           let y = new_temp ~name:x.name (ty_buffer n) in
           let yparts = list_map_n (fun _ -> Env.fresh_ident x.name) n in
           let assign_part e p act =
@@ -559,7 +559,7 @@ let transf_fundef env f =
          TVoid [],
          (vres, tres) :: params,
          transf_funbody env (subst_stmt subst f.fd_body) (Some eeres))
-    | Ret_value(ty, _, _) ->
+    | Ret_value(ty, sz, al) ->
         (f.fd_attrib,
          ty,
          params,
@@ -573,7 +573,7 @@ let transf_fundef env f =
 
 (* Composites *)
 
-let transf_composite env _ _ attr fl =
+let transf_composite env su id attr fl =
   (attr, List.map (fun f -> {f with fld_typ = transf_type env f.fld_typ}) fl)
 
 (* Entry point *)
@@ -591,5 +591,5 @@ let program p =
     ~decl:transf_decl
     ~fundef:transf_fundef
     ~composite:transf_composite
-    ~typedef:(fun env _ ty -> transf_type env ty)
+    ~typedef:(fun env id ty -> transf_type env ty)
     p
diff --git a/cparser/Transform.ml b/cparser/Transform.ml
index 685ef7e1..0a2ce3bb 100644
--- a/cparser/Transform.ml
+++ b/cparser/Transform.ml
@@ -141,7 +141,7 @@ let expand_postincrdecr ~read ~write env ctx op l =
    and preserving the statement structure.
    If [decl] is not given, it applies only to unblocked code. *)
 
-let stmt ~expr ?(decl = fun _ _ -> assert false) env s =
+let stmt ~expr ?(decl = fun env decl -> assert false) env s =
   let rec stm s =
   match s.sdesc with
   | Sskip -> s
@@ -163,7 +163,7 @@ let stmt ~expr ?(decl = fun _ _ -> assert false) env s =
       {s with sdesc = Sswitch(expr s.sloc env Val e, stm s1)}
   | Slabeled(lbl, s) ->
       {s with sdesc = Slabeled(lbl, stm s)}
-  | Sgoto _ -> s
+  | Sgoto lbl -> s
   | Sreturn None -> s
   | Sreturn (Some e) ->
       {s with sdesc = Sreturn(Some(expr s.sloc env Val e))}
@@ -191,12 +191,12 @@ let fundef trstmt env f =
 (* Generic transformation of a program *)
 
 let program
-    ?(decl = fun _ d -> d)
-    ?(fundef = fun _ fd -> fd)
-    ?(composite = fun _ _ _ attr fl -> (attr, fl))
-    ?(typedef = fun _ _ ty -> ty)
-    ?(enum = fun _ _ attr members -> (attr, members))
-    ?(pragma = fun _ s -> s)
+    ?(decl = fun env d -> d)
+    ?(fundef = fun env fd -> fd)
+    ?(composite = fun env su id attr fl -> (attr, fl))
+    ?(typedef = fun env id ty -> ty)
+    ?(enum = fun env id attr members -> (attr, members))
+    ?(pragma = fun env s -> s)
     p =
 
   let rec transf_globdecls env accu = function
@@ -204,7 +204,7 @@ let program
   | g :: gl ->
       let (desc', env') =
         match g.gdesc with
-        | Gdecl((sto, id, ty, _) as d) ->
+        | Gdecl((sto, id, ty, init) as d) ->
            (Gdecl(decl env d), Env.add_ident env id sto ty)
         | Gfundef f ->
            (Gfundef(fundef env f),
diff --git a/cparser/Unblock.ml b/cparser/Unblock.ml
index eaf49164..0669be6e 100644
--- a/cparser/Unblock.ml
+++ b/cparser/Unblock.ml
@@ -46,13 +46,13 @@ let rec local_initializer env path init k =
             (array_init (Int64.succ pos) il')
         end in
       array_init 0L il
-  | Init_struct(_, fil) ->
+  | Init_struct(id, fil) ->
       let field_init (fld, i) k =
         local_initializer env
           { edesc = EUnop(Odot fld.fld_name, path); etyp = fld.fld_typ }
           i k in
       List.fold_right field_init fil k
-  | Init_union(_, fld, i) ->
+  | Init_union(id, fld, i) ->
       local_initializer env
         { edesc = EUnop(Odot fld.fld_name, path); etyp = fld.fld_typ }
         i k
@@ -293,7 +293,7 @@ let rec unblock_stmt env ctx ploc s =
   | Slabeled(lbl, s1) ->
       add_lineno ctx ploc s.sloc
         {s with sdesc = Slabeled(lbl, unblock_stmt env ctx s.sloc s1)}
-  | Sgoto _ ->
+  | Sgoto lbl ->
       add_lineno ctx ploc s.sloc s
   | Sreturn None ->
       add_lineno ctx ploc s.sloc s
@@ -311,7 +311,7 @@ let rec unblock_stmt env ctx ploc s =
           id:: ctx
         else ctx in
       unblock_block env ctx' ploc sl
-  | Sdecl _ ->
+  | Sdecl d ->
       assert false
   | Sasm(attr, template, outputs, inputs, clob) ->
       let expand_asm_operand (lbl, cstr, e) =
diff --git a/driver/Driver.ml b/driver/Driver.ml
index 7b245e6e..16267128 100644
--- a/driver/Driver.ml
+++ b/driver/Driver.ml
@@ -58,7 +58,7 @@ let command ?stdout args =
     if stdout <> None then Unix.close fd_out;
     match status with
     | Unix.WEXITED rc -> rc
-    | Unix.WSIGNALED _ | Unix.WSTOPPED _ ->
+    | Unix.WSIGNALED n | Unix.WSTOPPED n ->
         eprintf "Command '%s' killed on a signal.\n" argv.(0); -1
   with Unix.Unix_error(err, fn, param) ->
     eprintf "Error executing '%s': %s: %s %s\n"
@@ -681,13 +681,13 @@ let cmdline_actions =
   Exact "-fall", Self (fun _ -> set_all language_support_options);
   Exact "-fnone", Self (fun _ -> unset_all language_support_options);
 (* Debugging options *)
-  Exact "-g", Self (fun _ -> option_g := true;
+  Exact "-g", Self (fun s -> option_g := true;
     option_gdwarf := 3);
-  Exact "-gdwarf-2", Self (fun _ -> option_g:=true;
+  Exact "-gdwarf-2", Self (fun s -> option_g:=true;
     option_gdwarf := 2);
-  Exact "-gdwarf-3", Self (fun _ -> option_g := true;
+  Exact "-gdwarf-3", Self (fun s -> option_g := true;
     option_gdwarf := 3);
-  Exact "-frename-static", Self (fun _ -> option_rename_static:= true);
+  Exact "-frename-static", Self (fun s -> option_rename_static:= true);
    Exact "-gdepth", Integer (fun n -> if n = 0 || n <0 then begin
      option_g := false
    end else begin
diff --git a/driver/Interp.ml b/driver/Interp.ml
index 8dd4a7c9..e3a7d3b8 100644
--- a/driver/Interp.ml
+++ b/driver/Interp.ml
@@ -81,7 +81,7 @@ let name_of_fundef prog fd =
   | [] -> "<unknown function>"
   | (id, Gfun fd') :: rem ->
       if fd == fd' then extern_atom id else find_name rem
-  | (_, Gvar _) :: rem ->
+  | (id, Gvar v) :: rem ->
       find_name rem
   in find_name prog.Csyntax.prog_defs
 
@@ -90,7 +90,7 @@ let name_of_function prog fn =
   | [] -> "<unknown function>"
   | (id, Gfun(Csyntax.Internal fn')) :: rem ->
       if fn == fn' then extern_atom id else find_name rem
-  | _ :: rem ->
+  | (id, _) :: rem ->
       find_name rem
   in find_name prog.Csyntax.prog_defs
 
@@ -118,22 +118,22 @@ let print_val_list p vl =
 
 let print_state p (prog, ge, s) =
   match s with
-  | State(f, s, _, e, _) ->
+  | State(f, s, k, e, m) ->
       PrintCsyntax.print_pointer_hook := print_pointer ge.genv_genv e;
       fprintf p "in function %s, statement@ @[<hv 0>%a@]"
               (name_of_function prog f)
               PrintCsyntax.print_stmt s
-  | ExprState(f, r, _, e, _) ->
+  | ExprState(f, r, k, e, m) ->
       PrintCsyntax.print_pointer_hook := print_pointer ge.genv_genv e;
       fprintf p "in function %s, expression@ @[<hv 0>%a@]"
               (name_of_function prog f)
               PrintCsyntax.print_expr r
-  | Callstate(fd, args, _, _) ->
+  | Callstate(fd, args, k, m) ->
       PrintCsyntax.print_pointer_hook := print_pointer ge.genv_genv Maps.PTree.empty;
       fprintf p "calling@ @[<hov 2>%s(%a)@]"
               (name_of_fundef prog fd)
               print_val_list args
-  | Returnstate(res, _, _) ->
+  | Returnstate(res, k, m) ->
       PrintCsyntax.print_pointer_hook := print_pointer ge.genv_genv Maps.PTree.empty;
       fprintf p "returning@ %a"
               print_val res
@@ -220,10 +220,10 @@ let rank_state = function
   | Stuckstate -> assert false
 
 let mem_state = function
-  | State(_, _, _, _, m) -> m
-  | ExprState(_, _, _, _, m) -> m
-  | Callstate(_, _, _, m) -> m
-  | Returnstate(_, _, m) -> m
+  | State(f, s, k, e, m) -> m
+  | ExprState(f, r, k, e, m) -> m
+  | Callstate(fd, args, k, m) -> m
+  | Returnstate(res, k, m) -> m
   | Stuckstate -> assert false
 
 let compare_state s1 s2 =
@@ -394,14 +394,14 @@ let do_external_function id sg ge w args m =
   | _ ->
       None
 
-let do_inline_assembly _ _ _ _ _ _ = None
+let do_inline_assembly txt sg ge w args m = None
 
 (* Implementing external functions producing observable events *)
 
 let rec world ge m =
   lazy (Determinism.World(world_io ge m, world_vload ge m, world_vstore ge m))
 
-and world_io _ _ _ _ =
+and world_io ge m id args =
   None
 
 and world_vload ge m chunk id ofs =
@@ -416,7 +416,7 @@ and world_vstore ge m chunk id ofs ev =
   Mem.store chunk m b ofs v >>= fun m' ->
   Some(world ge m')
 
-let do_event p _ time w ev =
+let do_event p ge time w ev =
   if !trace >= 1 then
     fprintf p "@[<hov 2>Time %d: observable event:@ %a@]@."
               time print_event ev;
@@ -438,30 +438,30 @@ let rec do_events p ge time w t =
 
 let (|||) a b = a || b (* strict boolean or *)
 
-let diagnose_stuck_expr p ge w _ a _ e m =
+let diagnose_stuck_expr p ge w f a kont e m =
   let rec diagnose k a =
   (* diagnose subexpressions first *)
   let found =
     match k, a with
-    | LV, Ederef(r, _) -> diagnose RV r
-    | LV, Efield(r, _, _) -> diagnose RV r
-    | RV, Evalof(l, _) -> diagnose LV l
-    | RV, Eaddrof(l, _) -> diagnose LV l
-    | RV, Eunop(_, r1, _) -> diagnose RV r1
-    | RV, Ebinop(_, r1, r2, _) -> diagnose RV r1 ||| diagnose RV r2
-    | RV, Ecast(r1, _) -> diagnose RV r1
-    | RV, Econdition(r1, _, _, _) -> diagnose RV r1
-    | RV, Eassign(l1, r2, _) -> diagnose LV l1 ||| diagnose RV r2
-    | RV, Eassignop(_, l1, r2, _, _) -> diagnose LV l1 ||| diagnose RV r2
-    | RV, Epostincr(_, l, _) -> diagnose LV l
-    | RV, Ecomma(r1, _, _) -> diagnose RV r1
-    | RV, Eparen(r1, _, _) -> diagnose RV r1
-    | RV, Ecall(r1, rargs, _) -> diagnose RV r1 ||| diagnose_list rargs
-    | RV, Ebuiltin(_, _, rargs, _) -> diagnose_list rargs
+    | LV, Ederef(r, ty) -> diagnose RV r
+    | LV, Efield(r, f, ty) -> diagnose RV r
+    | RV, Evalof(l, ty) -> diagnose LV l
+    | RV, Eaddrof(l, ty) -> diagnose LV l
+    | RV, Eunop(op, r1, ty) -> diagnose RV r1
+    | RV, Ebinop(op, r1, r2, ty) -> diagnose RV r1 ||| diagnose RV r2
+    | RV, Ecast(r1, ty) -> diagnose RV r1
+    | RV, Econdition(r1, r2, r3, ty) -> diagnose RV r1
+    | RV, Eassign(l1, r2, ty) -> diagnose LV l1 ||| diagnose RV r2
+    | RV, Eassignop(op, l1, r2, tyres, ty) -> diagnose LV l1 ||| diagnose RV r2
+    | RV, Epostincr(id, l, ty) -> diagnose LV l
+    | RV, Ecomma(r1, r2, ty) -> diagnose RV r1
+    | RV, Eparen(r1, tycast, ty) -> diagnose RV r1
+    | RV, Ecall(r1, rargs, ty) -> diagnose RV r1 ||| diagnose_list rargs
+    | RV, Ebuiltin(ef, tyargs, rargs, ty) -> diagnose_list rargs
     | _, _ -> false in
   if found then true else begin
     let l = Cexec.step_expr ge do_external_function do_inline_assembly e w k a m in
-    if List.exists (fun (_,red) -> red = Cexec.Stuckred) l then begin
+    if List.exists (fun (ctx,red) -> red = Cexec.Stuckred) l then begin
       PrintCsyntax.print_pointer_hook := print_pointer ge.genv_genv e;
       fprintf p "@[<hov 2>Stuck subexpression:@ %a@]@."
               PrintCsyntax.print_expr a;
@@ -496,7 +496,7 @@ let do_step p prog ge time s w =
   | None ->
       let l = Cexec.do_step ge do_external_function do_inline_assembly w s in
       if l = []
-      || List.exists (fun (Cexec.TR(_,_,s)) -> s = Stuckstate) l
+      || List.exists (fun (Cexec.TR(r,t,s)) -> s = Stuckstate) l
       then begin
         pp_set_max_boxes p 1000;
         fprintf p "@[<hov 2>Stuck state: %a@]@." print_state (prog, ge, s);
@@ -529,7 +529,7 @@ let rec explore_one p prog ge time s w =
 let rec explore_all p prog ge time states =
   if !trace >= 2 then begin
     List.iter
-      (fun (n, s, _) ->
+      (fun (n, s, w) ->
          fprintf p "@[<hov 2>State %d.%d: @ %a@]@."
                    time n print_state (prog, ge, s))
       states
@@ -579,7 +579,7 @@ let world_program prog =
           else
             {gv with gvar_init = []} in
         (id, Gvar gv')
-    | Gfun _ ->
+    | Gfun fd ->
         (id, gd) in
  {prog with Csyntax.prog_defs = List.map change_def prog.Csyntax.prog_defs}
 
@@ -604,7 +604,7 @@ let change_main_function p old_main old_main_ty =
 let rec find_main_function name = function
   | [] -> None
   | (id, Gfun fd) :: gdl -> if id = name then Some fd else find_main_function name gdl
-  | (_, Gvar _) :: gdl -> find_main_function name gdl
+  | (id, Gvar v) :: gdl -> find_main_function name gdl
 
 let fixup_main p =
   match find_main_function p.Csyntax.prog_main p.prog_defs with
diff --git a/exportclight/Clightgen.ml b/exportclight/Clightgen.ml
index ccdaabc4..d917032e 100644
--- a/exportclight/Clightgen.ml
+++ b/exportclight/Clightgen.ml
@@ -47,7 +47,7 @@ let command ?stdout args =
     if stdout <> None then Unix.close fd_out;
     match status with
     | Unix.WEXITED rc -> rc
-    | Unix.WSIGNALED _ | Unix.WSTOPPED _ ->
+    | Unix.WSIGNALED n | Unix.WSTOPPED n ->
         eprintf "Command '%s' killed on a signal.\n" argv.(0); -1
   with Unix.Unix_error(err, fn, param) ->
     eprintf "Error executing '%s': %s: %s %s\n"
@@ -186,7 +186,7 @@ let process_c_file sourcename =
 let explode_comma_option s =
   match Str.split (Str.regexp ",") s with
   | [] -> assert false
-  | _ :: tl -> tl
+  | hd :: tl -> tl
 
 let usage_string =
 "The CompCert Clight generator
diff --git a/exportclight/ExportClight.ml b/exportclight/ExportClight.ml
index 4ae6f1f5..a14b08d8 100644
--- a/exportclight/ExportClight.ml
+++ b/exportclight/ExportClight.ml
@@ -35,7 +35,7 @@ let print_list fn p l =
   match l with
   | [] ->
       fprintf p "nil"
-  | _ :: _ ->
+  | hd :: tl ->
       fprintf p "@[<hov 1>(";
       let rec plist = function
       | [] -> fprintf p "nil"
@@ -73,7 +73,7 @@ let ident p id =
 
 let iter_hashtbl_sorted (h: ('a, string) Hashtbl.t) (f: 'a * string -> unit) =
   List.iter f
-    (List.fast_sort (fun (_, d1) (_, d2) -> String.compare d1 d2)
+    (List.fast_sort (fun (k1, d1) (k2, d2) -> String.compare d1 d2)
       (Hashtbl.fold (fun k d accu -> (k, d) :: accu) h []))
 
 let define_idents p =
@@ -403,12 +403,12 @@ let print_globdef p (id, gd) =
   | Gvar v -> print_variable p (id, v)
 
 let print_ident_globdef p = function
-  | (id, Gfun(Clight.Internal _)) ->
+  | (id, Gfun(Clight.Internal f)) ->
       fprintf p "(%a, Gfun(Internal f_%s))" ident id (extern_atom id)
   | (id, Gfun(Clight.External(ef, targs, tres, cc))) ->
       fprintf p "@[<hov 2>(%a,@ @[<hov 2>Gfun(External %a@ %a@ %a@ %a))@]@]"
         ident id external_function ef typlist targs typ tres callconv cc
-  | (id, Gvar _) ->
+  | (id, Gvar v) ->
       fprintf p "(%a, Gvar v_%s)" ident id (extern_atom id)
 
 (* Composite definitions *)
@@ -449,7 +449,7 @@ let print_assertion p (txt, targs) =
     frags;
   fprintf p "  | \"%s\"%%string, " txt;
   list_iteri
-    (fun i _ -> fprintf p "_x%d :: " (i + 1))
+    (fun i targ -> fprintf p "_x%d :: " (i + 1))
     targs;
   fprintf p "nil =>@ ";
   fprintf p "    ";
@@ -481,20 +481,20 @@ Local Open Scope Z_scope.
 (* Naming the compiler-generated temporaries occurring in the program *)
 
 let rec name_expr = function
-  | Evar _ -> ()
-  | Etempvar(id, _) -> name_temporary id
-  | Ederef(a1, _) -> name_expr a1
-  | Efield(a1, _, _) -> name_expr a1
-  | Econst_int _ -> ()
-  | Econst_float _ -> ()
-  | Econst_long  _ -> ()
-  | Econst_single _ -> ()
-  | Eunop(_, a1, _) -> name_expr a1
-  | Eaddrof(a1, _) -> name_expr a1
-  | Ebinop(_, a1, a2, _) -> name_expr a1; name_expr a2
-  | Ecast(a1, _) -> name_expr a1
-  | Esizeof _ -> ()
-  | Ealignof _ -> ()
+  | Evar(id, t) -> ()
+  | Etempvar(id, t) -> name_temporary id
+  | Ederef(a1, t) -> name_expr a1
+  | Efield(a1, f, t) -> name_expr a1
+  | Econst_int(n, t) -> ()
+  | Econst_float(n, t) -> ()
+  | Econst_long(n, t) -> ()
+  | Econst_single(n, t) -> ()
+  | Eunop(op, a1, t) -> name_expr a1
+  | Eaddrof(a1, t) -> name_expr a1
+  | Ebinop(op, a1, a2, t) -> name_expr a1; name_expr a2
+  | Ecast(a1, t) -> name_expr a1
+  | Esizeof(t1, t) -> ()
+  | Ealignof(t1, t) -> ()
 
 let rec name_stmt = function
   | Sskip -> ()
@@ -502,7 +502,7 @@ let rec name_stmt = function
   | Sset(id, e2) -> name_temporary id; name_expr e2
   | Scall(optid, e1, el) ->
       name_opt_temporary optid; name_expr e1; List.iter name_expr el
-  | Sbuiltin(optid, _, _, el) ->
+  | Sbuiltin(optid, ef, tyl, el) ->
       name_opt_temporary optid; List.iter name_expr el
   | Ssequence(s1, s2) -> name_stmt s1; name_stmt s2
   | Sifthenelse(e, s1, s2) -> name_expr e; name_stmt s1; name_stmt s2
@@ -512,18 +512,18 @@ let rec name_stmt = function
   | Sswitch(e, cases) -> name_expr e; name_lblstmts cases
   | Sreturn (Some e) -> name_expr e
   | Sreturn None -> ()
-  | Slabel(_, s1) -> name_stmt s1
-  | Sgoto _ -> ()
+  | Slabel(lbl, s1) -> name_stmt s1
+  | Sgoto lbl -> ()
 
 and name_lblstmts = function
   | LSnil -> ()
-  | LScons(_, s, ls) -> name_stmt s; name_lblstmts ls
+  | LScons(lbl, s, ls) -> name_stmt s; name_lblstmts ls
 
 let name_function f =
-  List.iter (fun (id, _) -> name_temporary id) f.fn_temps;
+  List.iter (fun (id, ty) -> name_temporary id) f.fn_temps;
   name_stmt f.fn_body
 
-let name_globdef (_, g) =
+let name_globdef (id, g) =
   match g with
   | Gfun(Clight.Internal f) -> name_function f
   | _ -> ()
diff --git a/ia32/AsmToJSON.ml b/ia32/AsmToJSON.ml
index 60208fb3..3214491f 100644
--- a/ia32/AsmToJSON.ml
+++ b/ia32/AsmToJSON.ml
@@ -13,4 +13,5 @@
 (* Simple functions to serialize ia32 Asm to JSON *)
 
 (* Dummy function *)
-let p_program _ _ = ()
+let p_program oc prog =
+  ()
diff --git a/ia32/Asmexpand.ml b/ia32/Asmexpand.ml
index f2b6ad90..3a3548f9 100644
--- a/ia32/Asmexpand.ml
+++ b/ia32/Asmexpand.ml
@@ -93,7 +93,7 @@ let global_addr id ofs = Addrmode(None, None, Coq_inr(id, ofs))
 (* Unaligned memory accesses are quite fast on IA32, so use large
    memory accesses regardless of alignment. *)
 
-let expand_builtin_memcpy_small sz _ src dst =
+let expand_builtin_memcpy_small sz al src dst =
   let rec copy src dst sz =
     if sz >= 8 && !Clflags.option_ffpu then begin
 	emit (Pmovq_rm (XMM7, src));
@@ -114,7 +114,7 @@ let expand_builtin_memcpy_small sz _ src dst =
       end in
   copy (addressing_of_builtin_arg src) (addressing_of_builtin_arg dst) sz
 
-let expand_builtin_memcpy_big sz _ src dst =
+let expand_builtin_memcpy_big sz al src dst =
   if src <> BA (IR ESI) then emit (Plea (ESI, addressing_of_builtin_arg src));
   if dst <> BA (IR EDI) then emit (Plea (EDI, addressing_of_builtin_arg dst));
   emit (Pmov_ri (ECX,coqint_of_camlint (Int32.of_int (sz / 4))));
@@ -376,7 +376,7 @@ let expand_builtin_inline name args res =
 
 let expand_instruction instr =
   match instr with
-  | Pallocframe (sz, _, ofs_link) ->
+  | Pallocframe (sz, ofs_ra, ofs_link) ->
      let sz = sp_adjustment sz in
      let addr = linear_addr ESP (coqint_of_camlint (Int32.add sz 4l)) in
      let addr' = linear_addr ESP ofs_link in
@@ -386,13 +386,13 @@ let expand_instruction instr =
      emit (Plea (EDX,addr));
      emit (Pmov_mr (addr',EDX));
      PrintAsmaux.current_function_stacksize := sz
-  | Pfreeframe(sz, _, _) ->
+  | Pfreeframe(sz, ofs_ra, ofs_link) ->
      let sz = sp_adjustment sz in
      emit (Padd_ri (ESP,coqint_of_camlint sz))
   | Pbuiltin (ef,args, res) ->
      begin
        match ef with
-       | EF_builtin(name, _) ->
+       | EF_builtin(name, sg) ->
 	  expand_builtin_inline (camlstring_of_coqstring name) args res
        | EF_vload chunk ->
           expand_builtin_vload chunk args res
diff --git a/ia32/TargetPrinter.ml b/ia32/TargetPrinter.ml
index 246c01f3..f2358487 100644
--- a/ia32/TargetPrinter.ml
+++ b/ia32/TargetPrinter.ml
@@ -618,18 +618,18 @@ module Target(System: SYSTEM):TARGET =
       (* Pseudo-instructions *)
       | Plabel(l) ->
           fprintf oc "%a:\n" label (transl_label l)
-      | Pallocframe _
-      | Pfreeframe _ ->
+      | Pallocframe(sz, ofs_ra, ofs_link)
+      | Pfreeframe(sz, ofs_ra, ofs_link) ->
 	 assert false
       | Pbuiltin(ef, args, res) ->
           begin match ef with
-          | EF_annot(txt, _) ->
+          | EF_annot(txt, targs) ->
               fprintf oc "%s annotation: " comment;
               print_annot_text preg "%esp" oc (camlstring_of_coqstring txt) args
-          | EF_debug(kind, txt, _) ->
+          | EF_debug(kind, txt, targs) ->
               print_debug_info comment print_file_line preg "%esp" oc
                                (P.to_int kind) (extern_atom txt) args
-          | EF_inline_asm(txt, sg, _) ->
+          | EF_inline_asm(txt, sg, clob) ->
               fprintf oc "%s begin inline assembly\n\t" comment;
               print_inline_asm preg oc (camlstring_of_coqstring txt) sg args res;
               fprintf oc "%s end inline assembly\n" comment
diff --git a/powerpc/AsmToJSON.ml b/powerpc/AsmToJSON.ml
index dd7306fc..3d28c102 100644
--- a/powerpc/AsmToJSON.ml
+++ b/powerpc/AsmToJSON.ml
@@ -177,12 +177,12 @@ let p_instruction oc ic =
   | Pandi_ (ir1,ir2,c) -> instruction "Pandi_" [Ireg ir1; Ireg ir2; Constant c]
   | Pandis_ (ir1,ir2,c) -> instruction "Pandis_" [Ireg ir1; Ireg ir2; Constant c]
   | Pb l -> instruction "Pb" [ALabel l]
-  | Pbctr _ -> instruction "Pbctr" []
-  | Pbctrl _ -> instruction "Pbctrl" []
+  | Pbctr s -> instruction "Pbctr" []
+  | Pbctrl s -> instruction "Pbctrl" []
   | Pbdnz l -> instruction "Pbdnz" [ALabel l]
   | Pbf (cr,l) -> instruction "Pbf" [Crbit cr; ALabel l]
-  | Pbl (i,_) -> instruction "Pbl" [Atom i]
-  | Pbs (i,_) -> instruction "Pbs" [Atom i]
+  | Pbl (i,s) -> instruction "Pbl" [Atom i]
+  | Pbs (i,s) -> instruction "Pbs" [Atom i]
   | Pblr -> instruction "Pblr" []
   | Pbt (cr,l) ->  instruction "Pbt" [Crbit cr; ALabel l]
   | Pbtbl (i,lb) -> instruction "Pbtbl" ((Ireg i)::(List.map (fun a -> ALabel a) lb))
@@ -208,13 +208,13 @@ let p_instruction oc ic =
   | Pextsb (ir1,ir2) -> instruction "Pextsb" [Ireg ir1; Ireg ir2]
   | Pextsh (ir1,ir2) -> instruction "Pextsh" [Ireg ir1; Ireg ir2]
   | Pextsw (ir1,ir2) -> instruction "Pextsw" [Ireg ir1; Ireg ir2]
-  | Pfreeframe _ -> assert false (* Should not occur *)
+  | Pfreeframe (c,i) -> assert false (* Should not occur *)
   | Pfabs (fr1,fr2)
   | Pfabss (fr1,fr2) -> instruction "Pfabs" [Freg fr1; Freg fr2]
   | Pfadd (fr1,fr2,fr3) -> instruction "Pfadd" [Freg fr1; Freg fr2; Freg fr3]
   | Pfadds (fr1,fr2,fr3) -> instruction "Pfadds" [Freg fr1; Freg fr2; Freg fr3]
   | Pfcmpu (fr1,fr2) -> instruction "Pfcmpu" [Freg fr1; Freg fr2]
-  | Pfcfi _ -> () (* Should not occur *)
+  | Pfcfi (ir,fr) -> () (* Should not occur *)
   | Pfcfid (fr1,fr2) -> instruction "Pfcfid" [Freg fr1; Freg fr2]
   | Pfcfiu _ (* Should not occur *)
   | Pfcti _ (* Should not occur *)
@@ -224,14 +224,14 @@ let p_instruction oc ic =
   | Pfctiwz (fr1,fr2) -> instruction "Pfctiwz" [Freg fr1; Freg fr2]
   | Pfdiv (fr1,fr2,fr3) -> instruction "Pfdiv" [Freg fr1; Freg fr2; Freg fr3]
   | Pfdivs (fr1,fr2,fr3) -> instruction "Pfdivs" [Freg fr1; Freg fr2; Freg fr3]
-  | Pfmake _ -> ()(* Should not occur *)
+  | Pfmake (fr,ir1,ir2) -> ()(* Should not occur *)
   | Pfmr (fr1,fr2) -> instruction "Pfmr" [Freg fr1; Freg fr2]
   | Pfmul (fr1,fr2,fr3) -> instruction "Pfmul" [Freg fr1; Freg fr2; Freg fr3]
   | Pfmuls(fr1,fr2,fr3) -> instruction "Pfmuls" [Freg fr1; Freg fr2; Freg fr3]
   | Pfneg (fr1,fr2)
   | Pfnegs (fr1,fr2) -> instruction "Pfneg" [Freg fr1; Freg fr2]
   | Pfrsp (fr1,fr2) -> instruction "Pfrsp" [Freg fr1; Freg fr2]
-  | Pfxdp _ -> () (* Should not occur *)
+  | Pfxdp (fr1,fr2) -> () (* Should not occur *)
   | Pfsub (fr1,fr2,fr3) -> instruction "Pfsub" [Freg fr1; Freg fr2; Freg fr3]
   | Pfsubs (fr1,fr2,fr3) ->  instruction "Pfsubs" [Freg fr1; Freg fr2; Freg fr3]
   | Pfmadd (fr1,fr2,fr3,fr4) -> instruction "Pfmadd" [Freg fr1; Freg fr2; Freg fr3; Freg fr4]
@@ -271,7 +271,7 @@ let p_instruction oc ic =
   | Plwbrx (ir1,ir2,ir3) -> instruction "Plwbrx" [Ireg ir1; Ireg ir2; Ireg ir3]
   | Pmbar c -> instruction "Pmbar" [Constant (Cint c)]
   | Pmfcr ir -> instruction "Pmfcr" [Ireg ir]
-  | Pmfcrbit _ -> () (* Should not occur *)
+  | Pmfcrbit (ir,crb) -> () (* Should not occur *)
   | Pmflr ir -> instruction "Pmflr" [Ireg ir]
   | Pmr (ir1,ir2) -> instruction "Pmr" [Ireg ir1; Ireg ir2]
   | Pmtctr ir -> instruction "Pmtctr" [Ireg ir]
diff --git a/powerpc/Asmexpand.ml b/powerpc/Asmexpand.ml
index a6795030..86b74ab1 100644
--- a/powerpc/Asmexpand.ml
+++ b/powerpc/Asmexpand.ml
@@ -120,7 +120,7 @@ let memcpy_big_arg arg tmp =
   | _ ->
       assert false
 
-let expand_builtin_memcpy_big sz _ src dst =
+let expand_builtin_memcpy_big sz al src dst =
   assert (sz >= 4);
   emit_loadimm GPR0 (Z.of_uint (sz / 4));
   emit (Pmtctr GPR0);
@@ -721,7 +721,7 @@ let expand_instruction instr =
       emit (Prlwinm(r1, r1, Z.of_uint (1 + num_crbit bit), _1))
   | Pbuiltin(ef, args, res) ->
       begin match ef with
-      | EF_builtin(name, _) ->
+      | EF_builtin(name, sg) ->
           expand_builtin_inline (camlstring_of_coqstring name) args res
       | EF_vload chunk ->
           expand_builtin_vload chunk args res
diff --git a/powerpc/TargetPrinter.ml b/powerpc/TargetPrinter.ml
index 93d73d5c..99407da7 100644
--- a/powerpc/TargetPrinter.ml
+++ b/powerpc/TargetPrinter.ml
@@ -229,7 +229,7 @@ module Diab_System : SYSTEM =
       let name = name_of_section sec in
       assert (name <> "COMM");
       match sec with
-      | Section_debug_info (Some _) ->
+      | Section_debug_info (Some s) ->
           fprintf oc "	%s\n" name;
           fprintf oc "	.sectionlink	.debug_info\n"
       | _ ->
@@ -239,13 +239,13 @@ module Diab_System : SYSTEM =
       print_file_line_d2 oc comment file line
 
     (* Emit .cfi directives *)
-    let cfi_startproc _ = ()
+    let cfi_startproc oc = ()
 
-    let cfi_endproc _ = ()
+    let cfi_endproc oc = ()
 
-    let cfi_adjust _ _ = ()
+    let cfi_adjust oc delta = ()
 
-    let cfi_rel_offset _ _ _ = ()
+    let cfi_rel_offset oc reg ofs = ()
 
     let debug_section oc sec =
       match sec with
@@ -380,7 +380,7 @@ module Target (System : SYSTEM):TARGET =
           fprintf oc "	addis	%a, %a, %a\n" ireg r1 ireg_or_zero r2 constant c
       | Paddze(r1, r2) ->
           fprintf oc "	addze	%a, %a\n" ireg r1 ireg r2
-      | Pallocframe _ ->
+      | Pallocframe(sz, ofs, _) ->
           assert false
       | Pand_(r1, r2, r3) ->
           fprintf oc "	and.	%a, %a, %a\n" ireg r1 ireg r2 ireg r3
@@ -392,9 +392,9 @@ module Target (System : SYSTEM):TARGET =
           fprintf oc "	andis.	%a, %a, %a\n" ireg r1 ireg r2 constant c
       | Pb lbl ->
           fprintf oc "	b	%a\n" label (transl_label lbl)
-      | Pbctr _ ->
+      | Pbctr sg ->
           fprintf oc "	bctr\n"
-      | Pbctrl _ ->
+      | Pbctrl sg ->
           fprintf oc "	bctrl\n"
       | Pbdnz lbl ->
           fprintf oc "	bdnz	%a\n" label (transl_label lbl)
@@ -409,9 +409,9 @@ module Target (System : SYSTEM):TARGET =
             fprintf oc "	b	%a\n" label (transl_label lbl);
             fprintf oc "%a:\n" label next
           end
-      | Pbl(s, _) ->
+      | Pbl(s, sg) ->
           fprintf oc "	bl	%a\n" symbol s
-      | Pbs(s, _) ->
+      | Pbs(s, sg) ->
           fprintf oc "	b	%a\n" symbol s
       | Pblr ->
           fprintf oc "	blr\n"
@@ -483,7 +483,7 @@ module Target (System : SYSTEM):TARGET =
           fprintf oc "	extsh	%a, %a\n" ireg r1 ireg r2
       | Pextsw(r1, r2) ->
           fprintf oc "	extsw	%a, %a\n" ireg r1 ireg r2
-      | Pfreeframe _ ->
+      | Pfreeframe(sz, ofs) ->
           assert false
       | Pfabs(r1, r2) | Pfabss(r1, r2) ->
           fprintf oc "	fabs	%a, %a\n" freg r1 freg r2
@@ -493,17 +493,17 @@ module Target (System : SYSTEM):TARGET =
           fprintf oc "	fadds	%a, %a, %a\n" freg r1 freg r2 freg r3
       | Pfcmpu(r1, r2) ->
           fprintf oc "	fcmpu	%a, %a, %a\n" creg 0 freg r1 freg r2
-      | Pfcfi _ ->
+      | Pfcfi(r1, r2) ->
           assert false
       | Pfcfid(r1, r2) ->
           fprintf oc "	fcfid	%a, %a\n" freg r1 freg r2
-      | Pfcfiu _ ->
+      | Pfcfiu(r1, r2) ->
           assert false
-      | Pfcti _ ->
+      | Pfcti(r1, r2) ->
           assert false
       | Pfctidz(r1, r2) ->
           fprintf oc "	fctidz	%a, %a\n" freg r1 freg r2
-      | Pfctiu _ ->
+      | Pfctiu(r1, r2) ->
           assert false
       | Pfctiw(r1, r2) ->
           fprintf oc "	fctiw	%a, %a\n" freg r1 freg r2
@@ -513,7 +513,7 @@ module Target (System : SYSTEM):TARGET =
           fprintf oc "	fdiv	%a, %a, %a\n" freg r1 freg r2 freg r3
       | Pfdivs(r1, r2, r3) ->
           fprintf oc "	fdivs	%a, %a, %a\n" freg r1 freg r2 freg r3
-      | Pfmake _ ->
+      | Pfmake(rd, r1, r2) ->
           assert false
       | Pfmr(r1, r2) ->
           fprintf oc "	fmr	%a, %a\n" freg r1 freg r2
@@ -525,7 +525,7 @@ module Target (System : SYSTEM):TARGET =
           fprintf oc "	fneg	%a, %a\n" freg r1 freg r2
       | Pfrsp(r1, r2) ->
           fprintf oc "	frsp	%a, %a\n" freg r1 freg r2
-      | Pfxdp _ ->
+      | Pfxdp(r1, r2) ->
           assert false
       | Pfsub(r1, r2, r3) ->
           fprintf oc "	fsub	%a, %a, %a\n" freg r1 freg r2 freg r3
@@ -603,7 +603,7 @@ module Target (System : SYSTEM):TARGET =
           fprintf oc "	mbar	%ld\n" (camlint_of_coqint mo)
       | Pmfcr(r1) ->
           fprintf oc "	mfcr	%a\n" ireg r1
-      | Pmfcrbit _ ->
+      | Pmfcrbit(r1, bit) ->
           assert false
       | Pmflr(r1) ->
           fprintf oc "	mflr	%a\n" ireg r1
@@ -719,13 +719,13 @@ module Target (System : SYSTEM):TARGET =
           fprintf oc "%a:\n" label (transl_label lbl)
       | Pbuiltin(ef, args, res) ->
           begin match ef with
-          | EF_annot(txt, _) ->
+          | EF_annot(txt, targs) ->
               fprintf oc "%s annotation: " comment;
               print_annot_text preg_annot "r1" oc (camlstring_of_coqstring txt) args
-          | EF_debug(kind, txt, _) ->
+          | EF_debug(kind, txt, targs) ->
               print_debug_info comment print_file_line preg_annot "r1" oc
                                (P.to_int kind) (extern_atom txt) args
-          | EF_inline_asm(txt, sg, _) ->
+          | EF_inline_asm(txt, sg, clob) ->
               fprintf oc "%s begin inline assembly\n\t" comment;
               print_inline_asm preg oc (camlstring_of_coqstring txt) sg args res;
               fprintf oc "%s end inline assembly\n" comment
@@ -750,14 +750,14 @@ module Target (System : SYSTEM):TARGET =
        PowerPC instructions.  We can over-approximate. *)
 
     let instr_size = function
-      | Pbf _ -> 2
-      | Pbt _ -> 2
-      | Pbtbl _ -> 5
-      | Plfi _ -> 2
-      | Plfis _ -> 2
-      | Plabel _-> 0
-      | Pbuiltin ((EF_annot _ | EF_debug _), _, _) -> 0
-      | Pbuiltin _ -> 3
+      | Pbf(bit, lbl) -> 2
+      | Pbt(bit, lbl) -> 2
+      | Pbtbl(r, tbl) -> 5
+      | Plfi(r1, c) -> 2
+      | Plfis(r1, c) -> 2
+      | Plabel lbl -> 0
+      | Pbuiltin((EF_annot _ | EF_debug _), args, res) -> 0
+      | Pbuiltin(ef, args, res) -> 3
       | Pcfi_adjust _ | Pcfi_rel_offset _ -> 0
       | _ -> 1