Deactivate warning 27 and added back removed code.

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

15 files changed, 139 insertions, 139 deletions

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 =