From 5b05d3668571bd9b748b781b0cc29ae10f745f61 Mon Sep 17 00:00:00 2001
From: Bernhard Schommer <bernhardschommer@gmail.com>
Date: Thu, 10 Mar 2016 13:35:48 +0100
Subject: Code cleanup.

Removed some unused variables, functions etc. and resolved some
problems which occur if all warnings except 3,4,9 and 29 are active.
Bug 18394.
---
 backend/Linearizeaux.ml | 13 +++++--------
 1 file changed, 5 insertions(+), 8 deletions(-)

(limited to 'backend/Linearizeaux.ml')

diff --git a/backend/Linearizeaux.ml b/backend/Linearizeaux.ml
index 71ee2e56..41a98873 100644
--- a/backend/Linearizeaux.ml
+++ b/backend/Linearizeaux.ml
@@ -10,10 +10,7 @@
 (*                                                                     *)
 (* *********************************************************************)
 
-open Coqlib
-open Datatypes
 open LTL
-open Lattice
 open Maps
 open Camlcoq
 
@@ -82,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 (sig0, ros) :: _ -> end_block blk minpc
-       | Lcond (cond, args, ifso, ifnot) :: _ ->
+       | Ltailcall _ :: _ -> end_block blk minpc
+       | Lcond (_, _, ifso, ifnot) :: _ ->
              end_block blk minpc; start_block ifso; start_block ifnot
-       | Ljumptable(arg, tbl) :: _ ->
+       | Ljumptable(_, tbl) :: _ ->
              end_block blk minpc; List.iter start_block tbl
        | Lreturn :: _ -> end_block blk minpc
-       | instr :: b' -> do_instr_list b' in
+       | _ :: b' -> do_instr_list b' in
        do_instr_list b
   (* next_in_block: check if join point and either extend block
      or start block *)
@@ -113,5 +110,5 @@ let flatten_blocks blks =
 
 (* Build the enumeration *)
 
-let enumerate_aux f reach =
+let enumerate_aux f _ =
   flatten_blocks (basic_blocks f (join_points f))
-- 
cgit