Removing modules now unused

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

6 files changed, 0 insertions, 2822 deletions

diff --git a/backend/Coloring.v b/backend/Coloring.v
deleted file mode 100644
index a23bf55..0000000
--- a/backend/Coloring.v
+++ /dev/null
@@ -1,309 +0,0 @@
-(* *********************************************************************)
-(*                                                                     *)
-(*              The Compcert verified compiler                         *)
-(*                                                                     *)
-(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
-(*                                                                     *)
-(*  Copyright Institut National de Recherche en Informatique et en     *)
-(*  Automatique.  All rights reserved.  This file is distributed       *)
-(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
-(*                                                                     *)
-(* *********************************************************************)
-
-(** Construction and coloring of the interference graph. *)
-
-Require Import Coqlib.
-Require Import Maps.
-Require Import AST.
-Require Import Op.
-Require Import Registers.
-Require Import RTL.
-Require Import RTLtyping.
-Require Import Locations.
-Require Import Conventions.
-Require Import InterfGraph.
-
-(** * Construction of the interference graph *)
-
-(** Two registers interfere if there exists a program point where
-    they are both simultaneously live, and it is possible that they
-    contain different values at this program point.  Consequently,
-    two registers that do not interfere can be merged into one register
-    while preserving the program behavior: there is no program point
-    where this merged register would have to hold two different values
-    (for the two original registers), so to speak.
-
-    The simplified algorithm for constructing the interference graph
-    from the results of the liveness analysis is as follows:
-<<
-     start with empty interference graph
-     for each parameter p and register r live at the function entry point:
-         add conflict edge p <-> r 
-     for each instruction I in function:
-         let L be the live registers "after" I
-         if I is a "move" instruction  dst <- src, and dst is live:
-            add conflict edges dst <-> r for each r in L \ {dst, src}
-         else if I is an instruction with result dst, and dst is live:
-            add conflict edges dst <-> r for each r in L \ {dst};
-         if I is a "call" instruction dst <- f(args),
-            add conflict edges between all pseudo-registers in L \ {dst}
-            and all caller-save machine registers
-     done
->>
-    Notice that edges are added only when a register becomes live.
-    A register becomes live either if it is the result of an operation
-    (and is live afterwards), or if we are at the function entrance
-    and the register is a function parameter.  For two registers to
-    be simultaneously live at some program point, it must be the case
-    that one becomes live at a point where the other is already live.
-    Hence, it suffices to add interference edges between registers
-    that become live at some instruction and registers that are already
-    live at this instruction.  
-
-    Notice also the special treatment of ``move'' instructions:
-    since the destination register of the ``move'' is assigned the same value
-    as the source register, it is semantically correct to assign
-    the destination and the source registers to the same register,
-    even if the source register remains live afterwards.
-    (This is even desirable, since the ``move'' instruction can then
-    be eliminated.)  Thus, no interference is added between the
-    source and the destination of a ``move'' instruction.
-
-    Finally, for ``call'' instructions, we must make sure that
-    pseudo-registers live across the instruction are allocated to
-    callee-save machine register or to stack slots, but never to
-    caller-save machine registers (these lose their values across
-    the call).  We therefore add the corresponding conflict edges
-    between pseudo-registers live across and caller-save machine
-    registers (pairwise).  
-
-    The full algorithm is similar to the simplified algorithm above,
-    but records preference edges in addition to conflict edges.
-    Preference edges guide the graph coloring algorithm by telling it
-    that better code will be obtained eventually if it is possible
-    to allocate certain pseudo-registers to the same location or to
-    a given machine register.  Preference edges are added:
--   between the destination and source pseudo-registers of a ``move''
-    instruction;
--   between the arguments of a ``call'' instruction and the locations
-    of the arguments as dictated by the calling conventions;
--   between the result of a ``call'' instruction and the location
-    of the result as dictated by the calling conventions.
-*)
-
-Definition add_interf_live
-    (filter: reg -> bool) (res: reg) (live: Regset.t) (g: graph): graph :=
-  Regset.fold 
-    (fun r g => if filter r then add_interf r res g else g) live g.
-
-Definition add_interf_op
-    (res: reg) (live: Regset.t) (g: graph): graph :=
-  add_interf_live
-    (fun r => if Reg.eq r res then false else true)
-    res live g.
-
-Definition add_interf_move
-    (arg res: reg) (live: Regset.t) (g: graph): graph :=
-  add_interf_live
-    (fun r =>
-       if Reg.eq r res then false else
-       if Reg.eq r arg then false else true)
-    res live g.
-
-Definition add_interf_destroyed
-    (live: Regset.t) (destroyed: list mreg) (g: graph): graph :=
-  List.fold_left
-    (fun g mr => Regset.fold (fun r g => add_interf_mreg r mr g) live g)
-    destroyed g.
-
-Definition add_interfs_indirect_call
-    (rfun: reg) (locs: list loc) (g: graph): graph :=
-  List.fold_left
-    (fun g loc =>
-      match loc with R mr => add_interf_mreg rfun mr g | _ => g end)
-    locs g.
-
-Definition add_interf_call
-    (ros: reg + ident) (locs: list loc) (g: graph): graph :=
-  match ros with
-  | inl rfun => add_interfs_indirect_call rfun locs g
-  | inr idfun => g
-  end.
-
-Fixpoint add_prefs_call
-    (args: list reg) (locs: list loc) (g: graph) {struct args} : graph :=
-  match args, locs with
-  | a1 :: al, l1 :: ll =>
-      add_prefs_call al ll
-        (match l1 with R mr => add_pref_mreg a1 mr g | _ => g end)
-  | _, _ => g
-  end.
-
-Definition add_prefs_builtin (ef: external_function)
-                            (args: list reg) (res: reg) (g: graph) : graph :=
-  match ef, args with
-  | EF_annot_val txt targ, arg1 :: _ => add_pref arg1 res g
-  | _, _ => g
-  end.
-
-Definition add_interf_entry
-    (params: list reg) (live: Regset.t) (g: graph): graph :=
-  List.fold_left (fun g r => add_interf_op r live g) params g.
-
-Fixpoint add_interf_params
-    (params: list reg) (g: graph) {struct params}: graph :=
-  match params with
-  | nil => g
-  | p1 :: pl =>
-      add_interf_params pl
-        (List.fold_left
-          (fun g r => if Reg.eq r p1 then g else add_interf r p1 g)
-          pl g)
-  end.
-
-Definition add_edges_instr
-    (sig: signature) (i: instruction) (live: Regset.t) (g: graph) : graph :=
-  match i with
-  | Iop op args res s =>
-      if Regset.mem res live then
-        match is_move_operation op args with
-        | Some arg =>
-            add_pref arg res (add_interf_move arg res live g)
-        | None =>
-            add_interf_op res live g
-        end
-      else g
-  | Iload chunk addr args dst s =>
-      if Regset.mem dst live
-      then add_interf_op dst live g
-      else g
-  | Icall sig ros args res s =>
-      let largs := loc_arguments sig in
-      let lres := loc_result sig in
-      add_prefs_call args largs
-        (add_pref_mreg res lres
-          (add_interf_op res live
-            (add_interf_call ros largs
-              (add_interf_destroyed
-                (Regset.remove res live) destroyed_at_call_regs g))))
-  | Itailcall sig ros args =>
-      let largs := loc_arguments sig in
-      add_prefs_call args largs
-        (add_interf_call ros largs g)
-  | Ibuiltin ef args res s =>
-      add_prefs_builtin ef args res (add_interf_op res live g)
-  | Ireturn (Some r) =>
-      add_pref_mreg r (loc_result sig) g
-  | _ => g
-  end.
-
-Definition add_edges_instrs (f: function) (live: PMap.t Regset.t) : graph :=
-  PTree.fold
-    (fun g pc i => add_edges_instr f.(fn_sig) i live!!pc g)
-    f.(fn_code)
-    empty_graph.
-
-Definition interf_graph (f: function) (live: PMap.t Regset.t) (live0: Regset.t) :=
-  add_prefs_call f.(fn_params) (loc_parameters f.(fn_sig))
-    (add_interf_params f.(fn_params)
-      (add_interf_entry f.(fn_params) live0
-        (add_edges_instrs f live))).
-
-(** * Graph coloring *)
-
-(** The actual coloring of the graph is performed by a function written
-  directly in Caml, and not proved correct in any way.  This function
-  takes as argument the [RTL] function, the interference graph for
-  this function, an assignment of types to [RTL] pseudo-registers,
-  and the set of all [RTL] pseudo-registers mentioned in the
-  interference graph.  It returns the coloring as a function from
-  pseudo-registers to locations. *)
-
-Parameter graph_coloring: 
-  function -> graph -> regenv -> Regset.t -> (reg -> loc).
-
-(** To ensure that the result of [graph_coloring] is a correct coloring,
-  we check a posteriori its result using the following Coq functions.
-  Let [coloring] be the function [reg -> loc] returned by [graph_coloring].
-  The three properties checked are:
-- [coloring r1 <> coloring r2] if there is a conflict edge between
-  [r1] and [r2] in the interference graph.
-- [coloring r1 <> R m2] if there is a conflict edge between pseudo-register
-  [r1] and machine register [m2] in the interference graph.
-- For all [r] mentioned in the interference graph,
-  the location [coloring r] is acceptable and has the same type as [r].
-*)
-
-Definition check_coloring_1 (g: graph) (coloring: reg -> loc) :=
-  SetRegReg.for_all 
-    (fun r1r2 =>
-      if Loc.eq (coloring (fst r1r2)) (coloring (snd r1r2)) then false else true)
-    g.(interf_reg_reg).
-
-Definition check_coloring_2 (g: graph) (coloring: reg -> loc) :=
-  SetRegMreg.for_all 
-    (fun r1mr2 =>
-      if Loc.eq (coloring (fst r1mr2)) (R (snd r1mr2)) then false else true)
-    g.(interf_reg_mreg).
-
-Definition same_typ (t1 t2: typ) :=
-  match t1, t2 with
-  | Tint, Tint => true
-  | Tfloat, Tfloat => true
-  | _, _ => false
-  end.
-
-Definition loc_is_acceptable (l: loc) :=
-  match l with
-  | R r => 
-     if In_dec Loc.eq l temporaries then false else true
-  | S (Local ofs ty) =>
-     if zlt ofs 0 then false else true
-  | _ =>
-     false
-  end.
-
-Definition check_coloring_3 (rs: Regset.t) (env: regenv) (coloring: reg -> loc) :=
-  Regset.for_all
-    (fun r =>
-      let l := coloring r in
-      andb (loc_is_acceptable l) (same_typ (env r) (Loc.type l)))
-    rs.
-
-Definition check_coloring
-       (g: graph) (env: regenv) (rs: Regset.t) (coloring: reg -> loc) :=
-  andb (check_coloring_1 g coloring)
-       (andb (check_coloring_2 g coloring)
-             (check_coloring_3 rs env coloring)).
-
-(** To preserve decidability of checking, the checks
-  (especially the third one) are performed for the pseudo-registers
-  mentioned in the interference graph.  To facilitate the proofs,
-  it is convenient to ensure that the properties hold for all
-  pseudo-registers.  To this end, we ``clip'' the candidate coloring
-  returned by [graph_coloring]: the final coloring behave identically
-  over pseudo-registers mentioned in the interference graph,
-  but returns a dummy machine register of the correct type otherwise. *)
-
-Definition alloc_of_coloring (coloring: reg -> loc) (env: regenv) (rs: Regset.t) :=
-  fun r =>
-    if Regset.mem r rs
-    then coloring r
-    else match env r with Tint => R dummy_int_reg | Tfloat => R dummy_float_reg end.
-
-(** * Coloring of the interference graph *)
-
-(** The following function combines the phases described above:
-  construction of the interference graph, coloring by untrusted
-  Caml code, checking of the candidate coloring returned,
-  and adjustment of this coloring.  If the coloring candidate is
-  incorrect, [None] is returned, causing register allocation to fail. *)
-
-Definition regalloc
-    (f: function) (live: PMap.t Regset.t) (live0: Regset.t) (env: regenv) :=
-  let g := interf_graph f live live0 in
-  let rs := all_interf_regs g in
-  let coloring := graph_coloring f g env rs in
-  if check_coloring g env rs coloring
-  then Some (alloc_of_coloring coloring env rs)
-  else None.
diff --git a/backend/Coloringaux.ml b/backend/Coloringaux.ml
deleted file mode 100644
index 09ffb8e..0000000
--- a/backend/Coloringaux.ml
+++ /dev/null
@@ -1,867 +0,0 @@
-(* *********************************************************************)
-(*                                                                     *)
-(*              The Compcert verified compiler                         *)
-(*                                                                     *)
-(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
-(*                                                                     *)
-(*  Copyright Institut National de Recherche en Informatique et en     *)
-(*  Automatique.  All rights reserved.  This file is distributed       *)
-(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
-(*                                                                     *)
-(* *********************************************************************)
-
-open Camlcoq
-open Datatypes
-open AST
-open Maps
-open Registers
-open Machregs
-open Locations
-open RTL
-open RTLtyping
-open InterfGraph
-open Conventions1
-open Conventions
-
-(* George-Appel graph coloring *)
-
-(* \subsection{Internal representation of the interference graph} *)
-
-(* To implement George-Appel coloring, we first transform the representation
-   of the interference graph, switching to the following 
-   imperative representation that is well suited to the coloring algorithm. *)
-
-(* Each node of the graph (i.e. each pseudo-register) is represented as
-   follows. *)
-
-type node =
-  { ident: int;                         (*r unique identifier *)
-    typ: typ;                           (*r its type *)
-    regname: reg option;                (*r the RTL register it comes from *)
-    regclass: int;                      (*r identifier of register class *)
-    mutable accesses: int;              (*r number of defs and uses *)
-    mutable spillcost: float;           (*r estimated cost of spilling *)
-    mutable adjlist: node list;         (*r all nodes it interferes with *)
-    mutable degree: int;                (*r number of adjacent nodes *)
-    mutable movelist: move list;        (*r list of moves it is involved in *)
-    mutable alias: node option;         (*r [Some n] if coalesced with [n] *)
-    mutable color: loc option;          (*r chosen color *)
-    mutable nstate: nodestate;          (*r in which set of nodes it is *)
-    mutable nprev: node;                (*r for double linking *)
-    mutable nnext: node                 (*r for double linking *)
-  }
-
-(* These are the possible states for nodes. *)
-
-and nodestate =
-  | Colored
-  | Initial
-  | SimplifyWorklist
-  | FreezeWorklist
-  | SpillWorklist
-  | CoalescedNodes
-  | SelectStack
-
-(* Each move (i.e. wish to be put in the same location) is represented
-   as follows. *)
-
-and move =
-  { src: node;                          (*r source of the move *)
-    dst: node;                          (*r destination of the move *)
-    mutable mstate: movestate;          (*r in which set of moves it is *)
-    mutable mprev: move;                (*r for double linking *)
-    mutable mnext: move                 (*r for double linking *)
-  }
-
-(* These are the possible states for moves *)
-
-and movestate =
-  | CoalescedMoves
-  | ConstrainedMoves
-  | FrozenMoves
-  | WorklistMoves
-  | ActiveMoves
-
-(*i
-let name_of_node n =
-  match n.color, n.regname with
-  | Some(R r), _ ->
-      begin match Machregsaux.name_of_register r with
-                | None -> "fixed-reg"
-                | Some s -> s
-      end
-  | Some(S _), _ -> "fixed-slot"
-  | None, Some r -> Printf.sprintf "x%ld" (P.to_int32 r)
-  | None, None   -> "unknown-reg"
-*)
-
-(* The algorithm manipulates partitions of the nodes and of the moves
-   according to their states, frequently moving a node or a move from
-   a state to another, and frequently enumerating all nodes or all moves
-   of a given state.  To support these operations efficiently,
-   nodes or moves having the same state are put into imperative doubly-linked
-   lists, allowing for constant-time insertion and removal, and linear-time
-   scanning.  We now define the operations over these doubly-linked lists. *)
-
-module DLinkNode = struct
-  type t = node
-  let make state =
-    let rec empty =
-      { ident = 0; typ = Tint; regname = None; regclass = 0;
-        adjlist = []; degree = 0; accesses = 0; spillcost = 0.0;
-        movelist = []; alias = None; color = None;
-        nstate = state; nprev = empty; nnext = empty }
-    in empty
-  let dummy = make Colored
-  let clear dl = dl.nnext <- dl; dl.nprev <- dl
-  let notempty dl = dl.nnext != dl
-  let insert n dl =
-    n.nstate <- dl.nstate;
-    n.nnext <- dl.nnext; n.nprev <- dl;
-    dl.nnext.nprev <- n; dl.nnext <- n
-  let remove n dl =
-    assert (n.nstate = dl.nstate);
-    n.nnext.nprev <- n.nprev; n.nprev.nnext <- n.nnext
-  let move n dl1 dl2 =
-    remove n dl1; insert n dl2
-  let pick dl =
-    let n = dl.nnext in remove n dl; n
-  let iter f dl =
-    let rec iter n = if n != dl then (f n; iter n.nnext)
-    in iter dl.nnext
-  let fold f dl accu =
-    let rec fold n accu = if n == dl then accu else fold n.nnext (f n accu)
-    in fold dl.nnext accu
-end
-
-module DLinkMove = struct
-  type t = move
-  let make state =
-    let rec empty =
-      { src = DLinkNode.dummy; dst = DLinkNode.dummy; 
-        mstate = state; mprev = empty; mnext = empty }
-    in empty
-  let dummy = make CoalescedMoves
-  let clear dl = dl.mnext <- dl; dl.mprev <- dl
-  let notempty dl = dl.mnext != dl
-  let insert m dl =
-    m.mstate <- dl.mstate;
-    m.mnext <- dl.mnext; m.mprev <- dl;
-    dl.mnext.mprev <- m; dl.mnext <- m
-  let remove m dl =
-    assert (m.mstate = dl.mstate);
-    m.mnext.mprev <- m.mprev; m.mprev.mnext <- m.mnext
-  let move m dl1 dl2 =
-    remove m dl1; insert m dl2
-  let pick dl =
-    let m = dl.mnext in remove m dl; m
-  let iter f dl =
-    let rec iter m = if m != dl then (f m; iter m.mnext)
-    in iter dl.mnext
-  let fold f dl accu =
-    let rec fold m accu = if m == dl then accu else fold m.mnext (f m accu)
-    in fold dl.mnext accu
-end
-
-(* Auxiliary data structures *)
-
-module IntSet = Set.Make(struct
-  type t = int
-  let compare (x:int) (y:int) = compare x y
-end)
-
-module IntPairSet = Set.Make(struct
-  type t = int * int
-  let compare ((x1, y1): (int * int)) (x2, y2) =
-    if x1 < x2 then -1 else
-    if x1 > x2 then 1 else
-    if y1 < y2 then -1 else
-    if y1 > y2 then 1 else
-    0
-  end)
-
-(* Register classes *)
-
-let class_of_type = function Tint -> 0 | Tfloat -> 1
-
-let num_register_classes = 2
-
-let caller_save_registers = Array.make num_register_classes [||]
-
-let callee_save_registers = Array.make num_register_classes [||]
-
-let num_available_registers = Array.make num_register_classes 0
-
-let reserved_registers = ref ([]: mreg list)
-
-let allocatable_registers = ref ([]: mreg list)
-
-let rec remove_reserved = function
-  | [] -> []
-  | hd :: tl ->
-      if List.mem hd !reserved_registers
-      then remove_reserved tl
-      else hd :: remove_reserved tl
-
-let init_regs() =
-  let int_caller_save = remove_reserved int_caller_save_regs
-  and float_caller_save = remove_reserved float_caller_save_regs
-  and int_callee_save = remove_reserved int_callee_save_regs
-  and float_callee_save = remove_reserved float_callee_save_regs in
-  allocatable_registers :=
-    List.flatten [int_caller_save; float_caller_save;
-                  int_callee_save; float_callee_save];
-  caller_save_registers.(0) <- Array.of_list int_caller_save;
-  caller_save_registers.(1) <- Array.of_list float_caller_save;
-  callee_save_registers.(0) <- Array.of_list int_callee_save;
-  callee_save_registers.(1) <- Array.of_list float_callee_save;
-  for i = 0 to num_register_classes - 1 do
-    num_available_registers.(i) <-
-      Array.length caller_save_registers.(i)
-      + Array.length callee_save_registers.(i)
-  done
-
-(* \subsection{The George-Appel algorithm} *)
-
-(* Below is a straigthforward translation of the pseudo-code at the end
-   of the TOPLAS article by George and Appel.  Two bugs were fixed
-   and are marked as such.  Please refer to the article for explanations. *)
-
-(* The adjacency set  *)
-let adjSet = ref IntPairSet.empty
-
-(* Low-degree, non-move-related nodes *)
-let simplifyWorklist = DLinkNode.make SimplifyWorklist
-
-(* Low-degree, move-related nodes *)
-let freezeWorklist = DLinkNode.make FreezeWorklist
-
-(* High-degree nodes *)
-let spillWorklist = DLinkNode.make SpillWorklist
-
-(* Nodes that have been coalesced *)
-let coalescedNodes = DLinkNode.make CoalescedNodes
-
-(* Moves that have been coalesced *)
-let coalescedMoves = DLinkMove.make CoalescedMoves
-
-(* Moves whose source and destination interfere *)
-let constrainedMoves = DLinkMove.make ConstrainedMoves
-
-(* Moves that will no longer be considered for coalescing *)
-let frozenMoves = DLinkMove.make FrozenMoves
-
-(* Moves enabled for possible coalescing *)
-let worklistMoves = DLinkMove.make WorklistMoves
-
-(* Moves not yet ready for coalescing *)
-let activeMoves = DLinkMove.make ActiveMoves
-
-(* To generate node identifiers *)
-let nextRegIdent = ref 0
-
-(* Initialization of all global data structures *)
-
-let init_graph() =
-  adjSet := IntPairSet.empty;
-  nextRegIdent := 0;
-  DLinkNode.clear simplifyWorklist;
-  DLinkNode.clear freezeWorklist;
-  DLinkNode.clear spillWorklist;
-  DLinkNode.clear coalescedNodes;
-  DLinkMove.clear coalescedMoves;
-  DLinkMove.clear frozenMoves;
-  DLinkMove.clear worklistMoves;
-  DLinkMove.clear activeMoves
-
-(* Determine if two nodes interfere *)
-
-let interfere n1 n2 =
-  let i1 = n1.ident and i2 = n2.ident in
-  let p = if i1 < i2 then (i1, i2) else (i2, i1) in
-  IntPairSet.mem p !adjSet
-
-(* Add an edge to the graph.  Assume edge is not in graph already.
-   Do not add edges between nodes of different types. *)
-
-let addEdge n1 n2 =
-  if n1.typ = n2.typ then begin
-    (*i  Printf.printf "  %s -- %s;\n" (name_of_node n1) (name_of_node n2); *)
-    assert (n1 != n2 && not (interfere n1 n2));
-    let i1 = n1.ident and i2 = n2.ident in
-    let p = if i1 < i2 then (i1, i2) else (i2, i1) in
-    adjSet := IntPairSet.add p !adjSet;
-    if n1.nstate <> Colored then begin
-      n1.adjlist <- n2 :: n1.adjlist;
-      n1.degree  <- 1 + n1.degree
-    end;
-    if n2.nstate <> Colored then begin
-      n2.adjlist <- n1 :: n2.adjlist;
-      n2.degree  <- 1 + n2.degree
-    end
-  end
-
-(* Apply the given function to the relevant adjacent nodes of a node *)
-
-let iterAdjacent f n =
-  List.iter
-    (fun n ->
-      match n.nstate with
-      | SelectStack | CoalescedNodes -> ()
-      | _ -> f n)
-    n.adjlist
-
-(* Determine the moves affecting a node *)
-
-let moveIsActiveOrWorklist m =
-  match m.mstate with
-  | ActiveMoves | WorklistMoves -> true
-  | _ -> false
-
-let nodeMoves n =
-  List.filter moveIsActiveOrWorklist n.movelist
-
-(* Determine whether a node is involved in a move *)
-
-let moveRelated n =
-  List.exists moveIsActiveOrWorklist n.movelist
-
-(*i
-(* Check invariants *)
-
-let name_of_node n = string_of_int n.ident
-
-let degreeInvariant n =
-  let c = ref 0 in
-  iterAdjacent (fun n -> incr c) n;
-  if !c <> n.degree then
-    failwith("degree invariant violated by " ^ name_of_node n)
-
-let simplifyWorklistInvariant n =
-  if n.degree < num_available_registers.(n.regclass)
-  && not (moveRelated n)
-  then ()
-  else failwith("simplify worklist invariant violated by " ^ name_of_node n)
-
-let freezeWorklistInvariant n =
-  if n.degree < num_available_registers.(n.regclass)
-  && moveRelated n
-  then ()
-  else failwith("freeze worklist invariant violated by " ^ name_of_node n)
-
-let spillWorklistInvariant n =
-  if n.degree >= num_available_registers.(n.regclass)
-  then ()
-  else failwith("spill worklist invariant violated by " ^ name_of_node n)
-
-let checkInvariants () =
-  DLinkNode.iter
-    (fun n -> degreeInvariant n; simplifyWorklistInvariant n)
-    simplifyWorklist;
-  DLinkNode.iter
-    (fun n -> degreeInvariant n; freezeWorklistInvariant n)
-    freezeWorklist;
-  DLinkNode.iter
-    (fun n -> degreeInvariant n; spillWorklistInvariant n)
-    spillWorklist
-*)
-
-(* Build the internal representation of the graph *)
-
-let nodeOfReg r typenv spillcosts =
-  let ty = typenv r in
-  incr nextRegIdent;
-  let (acc, cost) = spillcosts r in
-  { ident = !nextRegIdent; typ = ty; 
-    regname = Some r; regclass = class_of_type ty;
-    accesses = acc; spillcost = float cost;
-    adjlist = []; degree = 0; movelist = []; alias = None;
-    color = None;
-    nstate = Initial;
-    nprev = DLinkNode.dummy; nnext = DLinkNode.dummy }
-
-let nodeOfMreg mr =
-  let ty = mreg_type mr in
-  incr nextRegIdent;
-  { ident = !nextRegIdent; typ = ty; 
-    regname = None; regclass = class_of_type ty;
-    accesses = 0; spillcost = 0.0;
-    adjlist = []; degree = 0; movelist = []; alias = None;
-    color = Some (R mr);
-    nstate = Colored;
-    nprev = DLinkNode.dummy; nnext = DLinkNode.dummy }
-
-let build g typenv spillcosts =
-  (* Associate an internal node to each pseudo-register and each location *)
-  let reg_mapping = Hashtbl.create 27
-  and mreg_mapping = Hashtbl.create 27 in
-  let find_reg_node r =
-    try
-      Hashtbl.find reg_mapping r
-    with Not_found ->
-      let n = nodeOfReg r typenv spillcosts in
-      Hashtbl.add reg_mapping r n;
-      n
-  and find_mreg_node mr =
-    try
-      Hashtbl.find mreg_mapping mr
-    with Not_found ->
-      let n = nodeOfMreg mr in
-      Hashtbl.add mreg_mapping mr n;
-      n in
-  (* Fill the adjacency set and the adjacency lists; compute the degrees. *)
-  SetRegReg.fold
-    (fun (r1, r2) () ->
-      addEdge (find_reg_node r1) (find_reg_node r2))
-    g.interf_reg_reg ();
-  SetRegMreg.fold
-    (fun (r1, mr2) () ->
-      addEdge (find_reg_node r1) (find_mreg_node mr2))
-    g.interf_reg_mreg ();
-  (* Process the moves and insert them in worklistMoves *)
-  let add_move n1 n2 =
-    (*i Printf.printf "  %s -- %s [color=\"red\"];\n" (name_of_node n1) (name_of_node n2); *)
-    let m =
-      { src = n1; dst = n2; mstate = WorklistMoves;
-        mnext = DLinkMove.dummy; mprev = DLinkMove.dummy } in
-    n1.movelist <- m :: n1.movelist;
-    n2.movelist <- m :: n2.movelist;
-    DLinkMove.insert m worklistMoves in
-  SetRegReg.fold
-    (fun (r1, r2) () ->
-      add_move (find_reg_node r1) (find_reg_node r2))
-    g.pref_reg_reg ();
-  SetRegMreg.fold
-    (fun (r1, mr2) () ->
-      let r1' = find_reg_node r1 in
-      if List.mem mr2 !allocatable_registers then
-        add_move r1' (find_mreg_node mr2))
-    g.pref_reg_mreg ();
-  (* Initial partition of nodes into spill / freeze / simplify *)
-  Hashtbl.iter
-    (fun r n ->
-      assert (n.nstate = Initial);
-      let k = num_available_registers.(n.regclass) in
-      if n.degree >= k then
-        DLinkNode.insert n spillWorklist
-      else if moveRelated n then
-        DLinkNode.insert n freezeWorklist
-      else
-        DLinkNode.insert n simplifyWorklist)
-    reg_mapping;
-  (* Return mapping from pseudo-registers to nodes *)
-  reg_mapping
-
-(* Enable moves that have become low-degree related *)
-
-let enableMoves n =
-  List.iter
-    (fun m ->
-      if m.mstate = ActiveMoves
-      then DLinkMove.move m activeMoves worklistMoves)
-    (nodeMoves n)
-
-(* Simulate the removal of a node from the graph *)
-
-let decrementDegree n =
-  let k = num_available_registers.(n.regclass) in
-  let d = n.degree in
-  n.degree <- d - 1;
-  if d = k then begin
-    enableMoves n;
-    iterAdjacent enableMoves n;
-(*    if n.nstate <> Colored then begin *)
-    if moveRelated n
-    then DLinkNode.move n spillWorklist freezeWorklist
-    else DLinkNode.move n spillWorklist simplifyWorklist
-(*    end *)
-  end
-
-(* Simulate the effect of combining nodes [n1] and [n3] on [n2],
-   where [n2] is a node adjacent to [n3]. *)
-
-let combineEdge n1 n2 =
-  assert (n1 != n2);
-  if interfere n1 n2 then begin
-    (* The two edges n2--n3 and n2--n1 become one, so degree of n2 decreases *)
-    decrementDegree n2
-  end else begin
-    (* Add new edge *)
-    let i1 = n1.ident and i2 = n2.ident in
-    let p = if i1 < i2 then (i1, i2) else (i2, i1) in
-    adjSet := IntPairSet.add p !adjSet;
-    if n1.nstate <> Colored then begin
-      n1.adjlist <- n2 :: n1.adjlist;
-      n1.degree  <- 1 + n1.degree
-    end;
-    if n2.nstate <> Colored then begin
-      n2.adjlist <- n1 :: n2.adjlist;
-      (* n2's degree stays the same because the old edge n2--n3 disappears
-         and becomes the new edge n2--n1 *)
-    end
-  end
-
-(* Simplification of a low-degree node *)
-
-let simplify () =
-  let n = DLinkNode.pick simplifyWorklist in
-  (*i Printf.printf "Simplifying %s\n" (name_of_node n); i*)
-  n.nstate <- SelectStack;
-  iterAdjacent decrementDegree n;
-  n
-
-(* Briggs's conservative coalescing criterion.  In the terminology of
-   Hailperin, "Comparing Conservative Coalescing Criteria",
-   TOPLAS 27(3) 2005, this is the full Briggs criterion, slightly
-   more powerful than the one in George and Appel's paper. *)
-
-let canCoalesceBriggs u v =
-  let seen = ref IntSet.empty in
-  let k = num_available_registers.(u.regclass) in
-  let c = ref 0 in
-  let consider other n =
-    if not (IntSet.mem n.ident !seen) then begin
-      seen := IntSet.add n.ident !seen;
-      (* if n interferes with both u and v, its degree will decrease by one
-         after coalescing *)
-      let degree_after_coalescing =
-        if interfere n other then n.degree - 1 else n.degree in
-      if degree_after_coalescing >= k then begin
-        incr c;
-        if !c >= k then raise Exit
-      end
-    end in
-  try
-    iterAdjacent (consider v) u;
-    iterAdjacent (consider u) v;
-    (*i Printf.printf "  Briggs: OK\n"; *)
-    true
-  with Exit ->
-    (*i Printf.printf "  Briggs: no\n"; *)
-    false
-
-(* George's conservative coalescing criterion: all high-degree neighbors
-   of [v] are neighbors of [u]. *)
-
-let canCoalesceGeorge u v =
-  let k = num_available_registers.(u.regclass) in
-  let isOK t =
-    if t.nstate = Colored then
-      if u.nstate = Colored || interfere t u then () else raise Exit
-    else
-      if t.degree < k || interfere t u then () else raise Exit
-  in
-  try
-    iterAdjacent isOK v;
-    (*i Printf.printf "  George: OK\n"; *)
-    true
-  with Exit ->
-    (*i Printf.printf "  George: no\n"; *)
-    false
-
-(* The combined coalescing criterion.  [u] can be precolored, but
-   [v] is not.  According to George and Appel's paper:
--  If [u] is precolored, use George's criterion.
--  If [u] is not precolored, use Briggs's criterion.
-
-   As noted by Hailperin, for non-precolored nodes, George's criterion 
-   is incomparable with Briggs's: there are cases where G says yes
-   and B says no.  Typically, [u] is a long-lived variable with many 
-   interferences, and [v] is a short-lived temporary copy of [u]
-   that has no more interferences than [u].  Coalescing [u] and [v]
-   is "weakly safe" in Hailperin's terminology: [u] is no harder to color,
-   [u]'s neighbors are no harder to color either, but if we end up
-   spilling [u], we'll spill [v] as well.  However, if [v] has at most
-   one def and one use, CompCert generates equivalent code if
-   both [u] and [v] are spilled and if [u] is spilled but not [v],
-   so George's criterion is safe in this case.  
-*)
-
-let thresholdGeorge = 2               (* = 1 def + 1 use *)
-
-let canCoalesce u v =
-  if u.nstate = Colored
-  then canCoalesceGeorge u v
-  else canCoalesceBriggs u v
-       || (v.accesses <= thresholdGeorge && canCoalesceGeorge u v)
-       || (u.accesses <= thresholdGeorge && canCoalesceGeorge v u)
-
-(* Update worklists after a move was processed *)
-
-let addWorkList u =
-  if (not (u.nstate = Colored))
-  && u.degree < num_available_registers.(u.regclass)
-  && (not (moveRelated u))
-  then DLinkNode.move u freezeWorklist simplifyWorklist
-
-(* Return the canonical representative of a possibly coalesced node *)
-
-let rec getAlias n =
-  match n.alias with None -> n | Some n' -> getAlias n'
-
-(* Combine two nodes *)
-
-let combine u v =
-  (*i  Printf.printf "Combining %s and %s\n" (name_of_node u) (name_of_node v); *)
-  if v.nstate = FreezeWorklist
-  then DLinkNode.move v freezeWorklist coalescedNodes
-  else DLinkNode.move v spillWorklist coalescedNodes;
-  v.alias <- Some u;
-  (* Precolored nodes often have big movelists, and if one of [u] and [v]
-     is precolored, it is []u.  So, append [v.movelist] to [u.movelist]
-     instead of the other way around. *)
-  u.movelist <- List.rev_append v.movelist u.movelist;
-  u.spillcost <- u.spillcost +. v.spillcost;
-  iterAdjacent (combineEdge u) v;  (*r original code using [decrementDegree] is buggy *)
-  enableMoves v;                   (*r added as per Appel's book erratum *)
-  if u.degree >= num_available_registers.(u.regclass)
-  && u.nstate = FreezeWorklist
-  then DLinkNode.move u freezeWorklist spillWorklist
-
-(* Attempt coalescing *)
-
-let coalesce () =
-  let m = DLinkMove.pick worklistMoves in
-  let x = getAlias m.src and y = getAlias m.dst in
-  let (u, v) = if y.nstate = Colored then (y, x) else (x, y) in
-  (*i Printf.printf "Attempt coalescing %s and %s\n" (name_of_node u) (name_of_node v); *)
-  if u == v then begin
-    DLinkMove.insert m coalescedMoves;
-    addWorkList u
-  end else if v.nstate = Colored || interfere u v then begin
-    DLinkMove.insert m constrainedMoves;
-    addWorkList u;
-    addWorkList v
-  end else if canCoalesce u v then begin
-    DLinkMove.insert m coalescedMoves;
-    combine u v;
-    addWorkList u
-  end else begin
-    DLinkMove.insert m activeMoves    
-  end
-
-(* Freeze moves associated with node [u] *)
-
-let freezeMoves u =
-  let u' = getAlias u in
-  let freeze m =
-    let y = getAlias m.src in
-    let v = if y == u' then getAlias m.dst else y in
-    DLinkMove.move m activeMoves frozenMoves;
-    if not (moveRelated v)
-    && v.degree < num_available_registers.(v.regclass)
-    && v.nstate <> Colored
-    then DLinkNode.move v freezeWorklist simplifyWorklist in
-  List.iter freeze (nodeMoves u)
-
-(* Pick a move and freeze it *)
-
-let freeze () =
-  let u = DLinkNode.pick freezeWorklist in
-  (*i  Printf.printf "Freezing %s\n" (name_of_node u);*)
-  DLinkNode.insert u simplifyWorklist;
-  freezeMoves u
-
-(* Chaitin's cost measure *)
-
-let spillCost n =
-(*i
-  Printf.printf "spillCost %s: uses = %.0f  degree = %d  cost = %f\n"
-                (name_of_node n) n.spillcost n.degree (n.spillcost /. float n.degree);
-*)
-  n.spillcost /. float n.degree
-
-(* Spill a node *)
-
-let selectSpill () =
-  (* Find a spillable node of minimal cost *)
-  let (n, cost) =
-    DLinkNode.fold
-      (fun n (best_node, best_cost as best) ->
-        let cost = spillCost n in
-        if cost < best_cost then (n, cost) else best)
-      spillWorklist (DLinkNode.dummy, infinity) in
-  assert (n != DLinkNode.dummy);
-  DLinkNode.remove n spillWorklist;
-  (*i Printf.printf "Spilling %s\n" (name_of_node n);*)
-  freezeMoves n;
-  n.nstate <- SelectStack;
-  iterAdjacent decrementDegree n;
-  n
-
-(* Produce the order of nodes that we'll use for coloring *)
-
-let rec nodeOrder stack =
-  (*i checkInvariants(); *)
-  if DLinkNode.notempty simplifyWorklist then
-    (let n = simplify() in nodeOrder (n :: stack))
-  else if DLinkMove.notempty worklistMoves then
-    (coalesce(); nodeOrder stack)
-  else if DLinkNode.notempty freezeWorklist then
-    (freeze(); nodeOrder stack)
-  else if DLinkNode.notempty spillWorklist then
-    (let n = selectSpill() in nodeOrder (n :: stack))
-  else
-    stack
-
-(* Assign a color (i.e. a hardware register or a stack location)
-   to a node.  The color is chosen among the colors that are not
-   assigned to nodes with which this node interferes.  The choice
-   is guided by the following heuristics: consider first caller-save
-   hardware register of the correct type; second, callee-save registers;
-   third, a stack location.  Callee-save registers and stack locations
-   are ``expensive'' resources, so we try to minimize their number
-   by picking the smallest available callee-save register or stack location.
-   In contrast, caller-save registers are ``free'', so we pick an
-   available one pseudo-randomly. *)
-
-module Locset =
-  Set.Make(struct type t = loc let compare = compare end)
-
-let start_points = Array.make num_register_classes 0
-
-let find_reg conflicts regclass =
-  let rec find avail curr last =
-    if curr >= last then None else begin
-      let l = R avail.(curr) in
-      if Locset.mem l conflicts
-      then find avail (curr + 1) last
-      else Some l
-    end in
-  let caller_save = caller_save_registers.(regclass)
-  and callee_save = callee_save_registers.(regclass)
-  and start = start_points.(regclass) in
-  match find caller_save start (Array.length caller_save) with
-  | Some _ as res ->
-      start_points.(regclass) <-
-        (if start + 1 < Array.length caller_save then start + 1 else 0);
-      res
-  | None ->
-      match find caller_save 0 start with
-      | Some _ as res ->
-          start_points.(regclass) <-
-            (if start + 1 < Array.length caller_save then start + 1 else 0);
-          res
-      | None ->
-          find callee_save 0 (Array.length callee_save)
-
-(* Aggressive coalescing of stack slots.  When assigning a slot,
-   try first the slots assigned to the temporaries for which we
-   have a preference, provided no conflict occurs. *)
-
-let rec reuse_slot conflicts n mvlist =
-  match mvlist with
-  | [] -> None
-  | mv :: rem ->
-      let attempt_reuse n' =
-        match n'.color with
-        | Some(S _ as l) when not (Locset.mem l conflicts) -> Some l
-        | _ -> reuse_slot conflicts n rem in
-      let src = getAlias mv.src and dst = getAlias mv.dst in
-      if n == src then attempt_reuse dst
-      else if n == dst then attempt_reuse src
-      else reuse_slot conflicts n rem (* should not happen? *)
-
-(* If no reuse possible, assign lowest nonconflicting stack slot. *)
-
-let find_slot conflicts typ =
-  let rec find curr =
-    let l = S(Local(curr, typ)) in
-    if Locset.mem l conflicts then find (Z.succ curr) else l
-  in find Z.zero
-
-let assign_color n =
-  let conflicts = ref Locset.empty in
-  List.iter
-    (fun n' ->
-      match (getAlias n').color with
-      | None -> ()
-      | Some l -> conflicts := Locset.add l !conflicts)
-    n.adjlist;
-  match find_reg !conflicts n.regclass with
-  | Some loc ->
-      n.color <- Some loc
-  | None ->
-      match reuse_slot !conflicts n n.movelist with
-      | Some loc ->
-          n.color <- Some loc
-      | None ->
-          n.color <- Some (find_slot !conflicts n.typ)
-
-(* Extract the location of a node *)
-
-let location_of_node n =
-  match n.color with
-  | None -> assert false
-  | Some loc -> loc
-
-(* Estimate spilling costs and counts the number of defs and uses.
-   Currently, we charge 10 for each access and 1 for each move.
-   To do: take loops into account. *)
-
-let spill_costs f =
-  let costs = ref (PMap.init (0,0)) in
-  let cost r =
-    PMap.get r !costs in
-  let charge amount r =
-    let (n, c) = cost r in
-    costs := PMap.set r (n + 1, c + amount) !costs in
-  let charge_list amount rl =
-    List.iter (charge amount) rl in
-  let charge_ros amount ros =
-    match ros with Coq_inl r -> charge amount r | Coq_inr _ -> () in
-  let process_instr () pc i =
-    match i with
-    | Inop _ -> ()
-    | Iop(Op.Omove, arg::nil, res, _) ->
-        charge 1 arg; charge 1 res
-    | Iop(op, args, res, _) ->
-        charge_list 10 args; charge 10 res
-    | Iload(chunk, addr, args, dst, _) ->
-        charge_list 10 args; charge 10 dst
-    | Istore(chunk, addr, args, src, _) ->
-        charge_list 10 args; charge 10 src
-    | Icall(sg, ros, args, res, _) ->
-        charge_ros 10 ros; charge_list 1 args; charge 1 res
-    | Itailcall(sg, ros, args) ->
-        charge_ros 10 ros; charge_list 1 args
-    | Ibuiltin(EF_annot _, args, res, _) ->
-        (* arguments are not actually used, so charge 0 for them;
-           result is not used but should not be spilled, so charge a lot *)
-        charge 1_000_000 res
-    | Ibuiltin(EF_annot_val _, args, res, _) -> 
-        (* like a move *)
-        charge_list 1 args; charge 1 res
-    | Ibuiltin((EF_vstore _|EF_vstore_global _|EF_memcpy _), args, res, _) ->
-        (* result is not used but should not be spilled, so charge a lot *)
-        charge_list 10 args; charge 1_000_000 res
-    | Ibuiltin(ef, args, res, _) ->
-        charge_list 10 args; charge 10 res
-    | Icond(cond, args, _, _) ->
-        charge_list 10 args
-    | Ijumptable(arg, _) ->
-        charge 10 arg
-    | Ireturn(Some r) ->
-        charge 1 r
-    | Ireturn None ->
-        () in
-  charge_list 1 f.fn_params;
-  PTree.fold process_instr f.fn_code ();
-  (* Result is cost function reg -> (num accesses, integer cost *)
-  cost
-
-(* This is the entry point for graph coloring. *)
-
-let graph_coloring (f: coq_function) (g: graph) (env: regenv) (regs: Regset.t)
-                   : (reg -> loc) =
-  init_regs();
-  init_graph();
-  Array.fill start_points 0 num_register_classes 0;
-  (*i Printf.printf "graph G {\n"; *)
-  let mapping = build g env (spill_costs f) in
-  (*i Printf.printf "}\n"; *)
-  List.iter assign_color (nodeOrder []);
-  init_graph();  (* free data structures *)
-  fun r ->
-    try location_of_node (getAlias (Hashtbl.find mapping r))
-    with Not_found -> R IT1 (* any location *)
diff --git a/backend/Coloringaux.mli b/backend/Coloringaux.mli
deleted file mode 100644
index 7597c7c..0000000
--- a/backend/Coloringaux.mli
+++ /dev/null
@@ -1,22 +0,0 @@
-(* *********************************************************************)
-(*                                                                     *)
-(*              The Compcert verified compiler                         *)
-(*                                                                     *)
-(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
-(*                                                                     *)
-(*  Copyright Institut National de Recherche en Informatique et en     *)
-(*  Automatique.  All rights reserved.  This file is distributed       *)
-(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
-(*                                                                     *)
-(* *********************************************************************)
-
-open Registers
-open Locations
-open RTL
-open RTLtyping
-open InterfGraph
-
-val graph_coloring:
-  coq_function -> graph -> regenv -> Regset.t -> (reg -> loc)
-
-val reserved_registers: Machregs.mreg list ref
diff --git a/backend/Coloringproof.v b/backend/Coloringproof.v
deleted file mode 100644
index 8ebc87e..0000000
--- a/backend/Coloringproof.v
+++ /dev/null
@@ -1,957 +0,0 @@
-(* *********************************************************************)
-(*                                                                     *)
-(*              The Compcert verified compiler                         *)
-(*                                                                     *)
-(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
-(*                                                                     *)
-(*  Copyright Institut National de Recherche en Informatique et en     *)
-(*  Automatique.  All rights reserved.  This file is distributed       *)
-(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
-(*                                                                     *)
-(* *********************************************************************)
-
-(** Correctness of graph coloring. *)
-
-Require Import SetoidList.
-Require Import Coqlib.
-Require Import Maps.
-Require Import AST.
-Require Import Op.
-Require Import Registers.
-Require Import RTL.
-Require Import RTLtyping.
-Require Import Locations.
-Require Import Conventions.
-Require Import InterfGraph.
-Require Import Coloring.
-
-(** * Correctness of the interference graph *)
-
-(** We show that the interference graph built by [interf_graph]
-  is correct in the sense that it contains all conflict edges
-  that we need.
-
-  Many boring lemmas on the auxiliary functions used to construct
-  the interference graph follow.  The lemmas are of two kinds:
-  the ``increasing'' lemmas show that the auxiliary functions only add 
-  edges to the interference graph, but do not remove existing edges;
-  and the ``correct'' lemmas show that the auxiliary functions
-  correctly add the edges that we'd like them to add. *)
-
-Lemma graph_incl_refl:
-  forall g, graph_incl g g.
-Proof.
-  intros; split; auto.
-Qed.
-
-Lemma add_interf_live_incl_aux:
-  forall (filter: reg -> bool) res live g,
-  graph_incl g
-    (List.fold_left
-      (fun g r => if filter r then add_interf r res g else g)
-      live g).
-Proof.
-  induction live; simpl; intros.
-  apply graph_incl_refl.
-  apply graph_incl_trans with (if filter a then add_interf a res g else g).
-  case (filter a).
-  apply add_interf_incl.
-  apply graph_incl_refl.
-  apply IHlive. 
-Qed.
-
-Lemma add_interf_live_incl:
-  forall (filter: reg -> bool) res live g,
-  graph_incl g (add_interf_live filter res live g).
-Proof.
-  intros. unfold add_interf_live. rewrite Regset.fold_1.
-  apply add_interf_live_incl_aux.
-Qed.
-
-Lemma add_interf_live_correct_aux:
-  forall filter res r live,
-  InA Regset.E.eq r live -> filter r = true ->
-  forall g,
-  interfere r res
-    (List.fold_left
-      (fun g r => if filter r then add_interf r res g else g)
-      live g).
-Proof.
-  induction 1; simpl; intros.
-  hnf in H. subst y. rewrite H0.
-  generalize (add_interf_live_incl_aux filter res l (add_interf r res g)).
-  intros [A B].
-  apply A. apply add_interf_correct.
-  apply IHInA; auto.
-Qed.
-
-Lemma add_interf_live_correct:
-  forall filter res live g r,
-  Regset.In r live ->
-  filter r = true ->
-  interfere r res (add_interf_live filter res live g).
-Proof.
-  intros.  unfold add_interf_live. rewrite Regset.fold_1.
-  apply add_interf_live_correct_aux; auto.
-  apply Regset.elements_1. auto.
-Qed.
-
-Lemma add_interf_op_incl: 
-  forall res live g,
-  graph_incl g (add_interf_op res live g).
-Proof.
-  intros; unfold add_interf_op. apply add_interf_live_incl.
-Qed.
-
-Lemma add_interf_op_correct:
-  forall res live g r,
-  Regset.In r live ->
-  r <> res ->
-  interfere r res (add_interf_op res live g).
-Proof.
-  intros.  unfold add_interf_op.
-  apply add_interf_live_correct.
-  auto. destruct (Reg.eq r res); congruence. 
-Qed.
-
-Lemma add_interf_move_incl: 
-  forall arg res live g,
-  graph_incl g (add_interf_move arg res live g).
-Proof.
-  intros; unfold add_interf_move. apply add_interf_live_incl.
-Qed.
-
-Lemma add_interf_move_correct:
-  forall arg res live g r,
-  Regset.In r live ->
-  r <> arg -> r <> res ->
-  interfere r res (add_interf_move arg res live g).
-Proof.
-  intros.  unfold add_interf_move.
-  apply add_interf_live_correct.
-  auto.
-  rewrite dec_eq_false; auto. rewrite dec_eq_false; auto.
-Qed.
-
-Lemma add_interf_destroyed_incl_aux_1:
-  forall mr live g,
-  graph_incl g
-    (List.fold_left (fun g r => add_interf_mreg r mr g) live g).
-Proof.
-  induction live; simpl; intros.
-  apply graph_incl_refl.
-  apply graph_incl_trans with (add_interf_mreg a mr g).
-  apply add_interf_mreg_incl.
-  auto.
-Qed.
-
-Lemma add_interf_destroyed_incl_aux_2:
-  forall mr live g,
-  graph_incl g
-    (Regset.fold (fun r g => add_interf_mreg r mr g) live g).
-Proof.
-  intros. rewrite Regset.fold_1. apply add_interf_destroyed_incl_aux_1.
-Qed.
-
-Lemma add_interf_destroyed_incl:
-  forall live destroyed g,
-  graph_incl g (add_interf_destroyed live destroyed g).
-Proof.
-  induction destroyed; simpl; intros.
-  apply graph_incl_refl.
-  eapply graph_incl_trans; [idtac|apply IHdestroyed].
-  apply add_interf_destroyed_incl_aux_2.
-Qed.
-
-Lemma add_interfs_indirect_call_incl:
-  forall rfun locs g,
-  graph_incl g (add_interfs_indirect_call rfun locs g).
-Proof.
-  unfold add_interfs_indirect_call. induction locs; simpl; intros.
-  apply graph_incl_refl.
-  destruct a. eapply graph_incl_trans; [idtac|eauto]. 
-  apply add_interf_mreg_incl.
-  auto.
-Qed.
-
-Lemma add_interfs_call_incl:
-  forall ros locs g,
-  graph_incl g (add_interf_call ros locs g).
-Proof.
-  intros. unfold add_interf_call. destruct ros.
-  apply add_interfs_indirect_call_incl.
-  apply graph_incl_refl.
-Qed.
-
-Lemma interfere_incl:
-  forall r1 r2 g1 g2,
-  graph_incl g1 g2 ->
-  interfere r1 r2 g1 ->
-  interfere r1 r2 g2.
-Proof.
-  unfold graph_incl; intros. elim H; auto.
-Qed.
-
-Lemma interfere_mreg_incl:
-  forall r1 r2 g1 g2,
-  graph_incl g1 g2 ->
-  interfere_mreg r1 r2 g1 ->
-  interfere_mreg r1 r2 g2.
-Proof.
-  unfold graph_incl; intros. elim H; auto.
-Qed.
-
-Lemma add_interf_destroyed_correct_aux_1:
-  forall mr r live,
-  InA Regset.E.eq r live ->
-  forall g,
-  interfere_mreg r mr
-    (List.fold_left (fun g r => add_interf_mreg r mr g) live g).
-Proof.
-  induction 1; simpl; intros.
-  hnf in H; subst y. eapply interfere_mreg_incl. 
-  apply add_interf_destroyed_incl_aux_1.
-  apply add_interf_mreg_correct.
-  auto.
-Qed.
-
-Lemma add_interf_destroyed_correct_aux_2:
-  forall mr live g r,
-  Regset.In r live ->
-  interfere_mreg r mr
-    (Regset.fold (fun r g => add_interf_mreg r mr g) live g).
-Proof.
-  intros. rewrite Regset.fold_1. apply add_interf_destroyed_correct_aux_1.
-  apply Regset.elements_1. auto.
-Qed.
-
-Lemma add_interf_destroyed_correct:
-  forall live destroyed g r mr,
-  Regset.In r live ->
-  In mr destroyed ->
-  interfere_mreg r mr (add_interf_destroyed live destroyed g).
-Proof.
-  induction destroyed; simpl; intros.
-  elim H0.
-  elim H0; intros. 
-  subst a. eapply interfere_mreg_incl.
-  apply add_interf_destroyed_incl.
-  apply add_interf_destroyed_correct_aux_2; auto.
-  apply IHdestroyed; auto.
-Qed.
-
-Lemma add_interfs_indirect_call_correct:
-  forall rfun mr locs g,
-  In (R mr) locs ->
-  interfere_mreg rfun mr (add_interfs_indirect_call rfun locs g).
-Proof.
-  unfold add_interfs_indirect_call. induction locs; simpl; intros.
-  elim H.
-  destruct H. subst a.
-  eapply interfere_mreg_incl.
-  apply (add_interfs_indirect_call_incl rfun locs (add_interf_mreg rfun mr g)).
-  apply add_interf_mreg_correct.
-  auto.
-Qed.
-
-Lemma add_interfs_call_correct:
-  forall rfun locs g mr,
-  In (R mr) locs -> 
-  interfere_mreg rfun mr (add_interf_call (inl _ rfun) locs g).
-Proof.
-  intros. unfold add_interf_call.
-  apply add_interfs_indirect_call_correct. auto.
-Qed.
-
-Lemma add_prefs_call_incl:
-  forall args locs g,
-  graph_incl g (add_prefs_call args locs g).
-Proof.
-  induction args; destruct locs; simpl; intros;
-  try apply graph_incl_refl.
-  destruct l. 
-  eapply graph_incl_trans; [idtac|eauto]. 
-  apply add_pref_mreg_incl.
-  auto.
-Qed.
-
-Lemma add_prefs_builtin_incl:
-  forall ef args res g,
-  graph_incl g (add_prefs_builtin ef args res g).
-Proof.
-  intros. unfold add_prefs_builtin. 
-  destruct ef; try apply graph_incl_refl.
-  destruct args; try apply graph_incl_refl.
-  apply add_pref_incl. 
-Qed.
-
-Lemma add_interf_entry_incl:
-  forall params live g,
-  graph_incl g (add_interf_entry params live g).
-Proof.
-  unfold add_interf_entry; induction params; simpl; intros.
-  apply graph_incl_refl.
-  eapply graph_incl_trans; [idtac|eauto].
-  apply add_interf_op_incl.
-Qed.
-
-Lemma add_interf_entry_correct:
-  forall params live g r1 r2,
-  In r1 params ->
-  Regset.In r2 live ->
-  r1 <> r2 ->
-  interfere r1 r2 (add_interf_entry params live g).
-Proof.
-  unfold add_interf_entry; induction params; simpl; intros.
-  elim H.
-  elim H; intro.
-  subst a. apply interfere_incl with (add_interf_op r1 live g).
-  exact (add_interf_entry_incl _ _ _).
-  apply interfere_sym. apply add_interf_op_correct; auto.
-  auto.
-Qed.
-
-Lemma add_interf_params_incl_aux:
-  forall p1 pl g,
-  graph_incl g
-   (List.fold_left
-      (fun g r => if Reg.eq r p1 then g else add_interf r p1 g)
-      pl g).
-Proof.
-  induction pl; simpl; intros.
-  apply graph_incl_refl.
-  eapply graph_incl_trans; [idtac|eauto].
-  case (Reg.eq a p1); intro.
-  apply graph_incl_refl. apply add_interf_incl.
-Qed.
-
-Lemma add_interf_params_incl:
-  forall pl g,
-  graph_incl g (add_interf_params pl g).
-Proof.
-  induction pl; simpl; intros.
-  apply graph_incl_refl.
-  eapply graph_incl_trans; [idtac|eauto].
-  apply add_interf_params_incl_aux.
-Qed.
-
-Lemma add_interf_params_correct_aux:
-  forall p1 pl g p2,
-  In p2 pl ->
-  p1 <> p2 ->
-  interfere p1 p2
-   (List.fold_left
-      (fun g r => if Reg.eq r p1 then g else add_interf r p1 g)
-      pl g).
-Proof.
-  induction pl; simpl; intros.
-  elim H.
-  elim H; intro; clear H.
-  subst a. apply interfere_sym. eapply interfere_incl.
-  apply add_interf_params_incl_aux. 
-  case (Reg.eq p2 p1); intro.
-  congruence. apply add_interf_correct.
-  auto.
-Qed.
-
-Lemma add_interf_params_correct:
-  forall pl g r1 r2,
-  In r1 pl -> In r2 pl -> r1 <> r2 ->
-  interfere r1 r2 (add_interf_params pl g).
-Proof.
-  induction pl; simpl; intros.
-  elim H.
-  elim H; intro; clear H; elim H0; intro; clear H0.
-  congruence.
-  subst a. eapply interfere_incl. apply add_interf_params_incl.
-  apply add_interf_params_correct_aux; auto.
-  subst a. apply interfere_sym.
-  eapply interfere_incl. apply add_interf_params_incl.
-  apply add_interf_params_correct_aux; auto.
-  auto.
-Qed.
-
-Lemma add_edges_instr_incl:
-  forall sig instr live g,
-  graph_incl g (add_edges_instr sig instr live g).
-Proof.
-  intros. destruct instr; unfold add_edges_instr;
-  try apply graph_incl_refl.
-  case (Regset.mem r live).
-  destruct (is_move_operation o l).
-  eapply graph_incl_trans; [idtac|apply add_pref_incl].
-  apply add_interf_move_incl.
-  apply add_interf_op_incl.
-  apply graph_incl_refl.
-  case (Regset.mem r live).
-  apply add_interf_op_incl.
-  apply graph_incl_refl.
-  eapply graph_incl_trans; [idtac|apply add_prefs_call_incl].
-  eapply graph_incl_trans; [idtac|apply add_pref_mreg_incl].
-  eapply graph_incl_trans; [idtac|apply add_interf_op_incl].
-  eapply graph_incl_trans; [idtac|apply add_interfs_call_incl].
-  apply add_interf_destroyed_incl.
-  eapply graph_incl_trans; [idtac|apply add_prefs_call_incl].
-  apply add_interfs_call_incl.
-  eapply graph_incl_trans. apply add_interf_op_incl. apply add_prefs_builtin_incl.
-  destruct o.
-  apply add_pref_mreg_incl.
-  apply graph_incl_refl.
-Qed.
-
-(** The proposition below states that graph [g] contains
-  all the conflict edges expected for instruction [instr]. *)
-
-Definition correct_interf_instr
-    (live: Regset.t) (instr: instruction) (g: graph) : Prop :=
-  match instr with
-  | Iop op args res s =>
-      match is_move_operation op args with
-      | Some arg =>
-          forall r,
-          Regset.In res live ->
-          Regset.In r live ->
-          r <> res -> r <> arg -> interfere r res g
-      | None =>
-          forall r,
-          Regset.In res live ->
-          Regset.In r live ->
-          r <> res -> interfere r res g
-      end
-  | Iload chunk addr args res s =>
-      forall r,
-      Regset.In res live ->
-      Regset.In r live ->
-      r <> res -> interfere r res g
-  | Icall sig ros args res s =>
-      (forall r mr,
-        Regset.In r live ->
-        In mr destroyed_at_call_regs ->
-        r <> res ->
-        interfere_mreg r mr g)
-   /\ (forall r,
-        Regset.In r live ->
-       r <> res -> interfere r res g)
-   /\ (match ros with
-       | inl rfun => forall mr, In (R mr) (loc_arguments sig) -> 
-                                interfere_mreg rfun mr g
-       | inr idfun => True
-       end)
-  | Itailcall sig ros args =>
-      match ros with
-        | inl rfun => forall mr, In (R mr) (loc_arguments sig) -> 
-                                 interfere_mreg rfun mr g
-        | inr idfun => True
-      end
-  | Ibuiltin ef args res s =>
-      forall r,
-      Regset.In r live ->
-      r <> res -> interfere r res g
-  | _ =>
-      True
-  end.
-
-Lemma correct_interf_instr_incl:
-  forall live instr g1 g2,
-  graph_incl g1 g2 ->
-  correct_interf_instr live instr g1 ->
-  correct_interf_instr live instr g2.
-Proof.
-  intros until g2. intro. 
-  unfold correct_interf_instr; destruct instr; auto.
-  destruct (is_move_operation o l).
-  intros. eapply interfere_incl; eauto.
-  intros. eapply interfere_incl; eauto.
-  intros. eapply interfere_incl; eauto.
-  intros [A [B C]].
-  split. intros. eapply interfere_mreg_incl; eauto.
-  split. intros. eapply interfere_incl; eauto.
-  destruct s0; auto. intros. eapply interfere_mreg_incl; eauto. 
-  destruct s0; auto. intros. eapply interfere_mreg_incl; eauto.
-  intros. eapply interfere_incl; eauto. 
-Qed.
-
-Lemma add_edges_instr_correct:
-  forall sig instr live g,
-  correct_interf_instr live instr (add_edges_instr sig instr live g).
-Proof.
-  intros.
-  destruct instr; unfold add_edges_instr; unfold correct_interf_instr; auto.
-  destruct (is_move_operation o l); intros.
-  rewrite Regset.mem_1; auto. eapply interfere_incl. 
-  apply add_pref_incl. apply add_interf_move_correct; auto.
-  rewrite Regset.mem_1; auto. apply add_interf_op_correct; auto. 
-
-  intros. rewrite Regset.mem_1; auto. apply add_interf_op_correct; auto.
-
-  (* Icall *)
-  set (largs := loc_arguments s).
-  set (lres := loc_result s).
-  split. intros.
-  apply interfere_mreg_incl with
-    (add_interf_destroyed (Regset.remove r live) destroyed_at_call_regs g).
-  eapply graph_incl_trans; [idtac|apply add_prefs_call_incl].
-  eapply graph_incl_trans; [idtac|apply add_pref_mreg_incl].
-  eapply graph_incl_trans; [idtac|apply add_interf_op_incl].
-  apply add_interfs_call_incl.
-  apply add_interf_destroyed_correct; auto.
-  apply Regset.remove_2; auto.
-
-  split. intros.
-  eapply interfere_incl.
-  eapply graph_incl_trans; [idtac|apply add_prefs_call_incl].
-  apply add_pref_mreg_incl.
-  apply add_interf_op_correct; auto.
-
-  destruct s0; auto; intros.
-  eapply interfere_mreg_incl.
-  eapply graph_incl_trans; [idtac|apply add_prefs_call_incl].
-  eapply graph_incl_trans; [idtac|apply add_pref_mreg_incl].
-  apply add_interf_op_incl.
-  apply add_interfs_call_correct. auto.
-
-  (* Itailcall *)
-  destruct s0; auto; intros.
-  eapply interfere_mreg_incl.
-  apply add_prefs_call_incl.
-  apply add_interfs_call_correct. auto.
-
-  (* Ibuiltin *)
-  intros. eapply interfere_incl. apply add_prefs_builtin_incl. 
-  apply add_interf_op_correct; auto. 
-Qed.
-
-Lemma add_edges_instrs_correct:
-  forall f live pc i,
-  f.(fn_code)!pc = Some i ->
-  correct_interf_instr live!!pc i (add_edges_instrs f live).
-Proof.
-  intros f live.
-  set (P := fun (c: code) g =>
-         forall pc i, c!pc = Some i -> correct_interf_instr live#pc i g).
-  set (F := (fun (g : graph) (pc0 : positive) (i0 : instruction) =>
-         add_edges_instr (fn_sig f) i0 live # pc0 g)).
-  change (P f.(fn_code) (PTree.fold F f.(fn_code) empty_graph)).
-  apply PTree_Properties.fold_rec; unfold P; intros.
-  apply H0. rewrite H. auto.
-  rewrite PTree.gempty in H. congruence.
-  rewrite PTree.gsspec in H2. destruct (peq pc k). 
-  inv H2. unfold F. apply add_edges_instr_correct. 
-  apply correct_interf_instr_incl with a. 
-  unfold F; apply add_edges_instr_incl.
-  apply H1; auto.
-Qed.
-
-(** Here are the three correctness properties of the generated
-  inference graph.  First, it contains the conflict edges
-  needed by every instruction of the function. *)
-
-Lemma interf_graph_correct_1:
-  forall f live live0 pc i,
-  f.(fn_code)!pc = Some i ->
-  correct_interf_instr live!!pc i (interf_graph f live live0).
-Proof.
-  intros. unfold interf_graph.
-  apply correct_interf_instr_incl with (add_edges_instrs f live).
-  eapply graph_incl_trans; [idtac|apply add_prefs_call_incl].
-  eapply graph_incl_trans; [idtac|apply add_interf_params_incl].
-  apply add_interf_entry_incl.
-  apply add_edges_instrs_correct; auto.
-Qed.
-
-(** Second, function parameters conflict pairwise. *)
-
-Lemma interf_graph_correct_2:
-  forall f live live0 r1 r2,
-  In r1 f.(fn_params) ->
-  In r2 f.(fn_params) ->
-  r1 <> r2 ->
-  interfere r1 r2 (interf_graph f live live0).
-Proof.
-  intros. unfold interf_graph. 
-  eapply interfere_incl.
-  apply add_prefs_call_incl.
-  apply add_interf_params_correct; auto.
-Qed.
-
-(** Third, function parameters conflict pairwise with pseudo-registers
-  live at function entry.  If the function never uses a pseudo-register
-  before it is defined, pseudo-registers live at function entry
-  are a subset of the function parameters and therefore this condition
-  is implied by [interf_graph_correct_3].  However, we prefer not
-  to make this assumption. *)
-
-Lemma interf_graph_correct_3:
-  forall f live live0 r1 r2,
-  In r1 f.(fn_params) ->
-  Regset.In r2 live0 ->
-  r1 <> r2 ->
-  interfere r1 r2 (interf_graph f live live0).
-Proof.
-  intros. unfold interf_graph.
-  eapply interfere_incl.
-  eapply graph_incl_trans; [idtac|apply add_prefs_call_incl].
-  apply add_interf_params_incl.
-  apply add_interf_entry_correct; auto.
-Qed.
-
-(** * Correctness of the a priori checks over the result of graph coloring *)
-
-(** We now show that the checks performed over the candidate coloring
-  returned by [graph_coloring] are correct: candidate colorings that
-  pass these checks are indeed correct colorings. *)
-
-Section CORRECT_COLORING.
-
-Variable g: graph.
-Variable env: regenv.
-Variable allregs: Regset.t.
-Variable coloring: reg -> loc.
-
-Lemma check_coloring_1_correct:
-  forall r1 r2,
-  check_coloring_1 g coloring = true ->
-  SetRegReg.In (r1, r2) g.(interf_reg_reg) ->
-  coloring r1 <> coloring r2.
-Proof.
-  unfold check_coloring_1. intros. 
-  assert (compat_bool OrderedRegReg.eq
-     (fun r1r2 => if Loc.eq (coloring (fst r1r2)) (coloring (snd r1r2))
-                  then false else true)).
-  red. unfold OrderedRegReg.eq. unfold OrderedReg.eq.
-  intros x y [EQ1 EQ2]. rewrite EQ1; rewrite EQ2; auto.
-  generalize (SetRegReg.for_all_2 H1 H H0). 
-  simpl. case (Loc.eq (coloring r1) (coloring r2)); intro.
-  intro; discriminate. auto.
-Qed.
-
-Lemma check_coloring_2_correct:
-  forall r1 mr2,
-  check_coloring_2 g coloring = true ->
-  SetRegMreg.In (r1, mr2) g.(interf_reg_mreg) ->
-  coloring r1 <> R mr2.
-Proof.
-  unfold check_coloring_2. intros. 
-  assert (compat_bool OrderedRegMreg.eq
-     (fun r1r2 => if Loc.eq (coloring (fst r1r2)) (R (snd r1r2))
-                  then false else true)).
-  red. unfold OrderedRegMreg.eq. unfold OrderedReg.eq.
-  intros x y [EQ1 EQ2]. rewrite EQ1; rewrite EQ2; auto.
-  generalize (SetRegMreg.for_all_2 H1 H H0). 
-  simpl. case (Loc.eq (coloring r1) (R mr2)); intro.
-  intro; discriminate. auto.
-Qed.
-
-Lemma same_typ_correct:
-  forall t1 t2, same_typ t1 t2 = true -> t1 = t2.
-Proof.
-  destruct t1; destruct t2; simpl; congruence.
-Qed.
-
-Lemma loc_is_acceptable_correct:
-  forall l, loc_is_acceptable l = true -> loc_acceptable l.
-Proof.
-  destruct l; unfold loc_is_acceptable, loc_acceptable.
-  case (In_dec Loc.eq (R m) temporaries); intro.
-  intro; discriminate. auto.
-  destruct s.
-  case (zlt z 0); intro. intro; discriminate. auto.
-  intro; discriminate.
-  intro; discriminate.
-Qed.
-
-Lemma check_coloring_3_correct:
-  forall r,
-  check_coloring_3 allregs env coloring = true ->
-  Regset.mem r allregs = true ->
-  loc_acceptable (coloring r) /\ env r = Loc.type (coloring r).
-Proof.
-  unfold check_coloring_3; intros.
-  exploit Regset.for_all_2; eauto.
-  red; intros. congruence.
-  apply Regset.mem_2. eauto.
-  simpl. intro. elim (andb_prop _ _ H1); intros.
-  split. apply loc_is_acceptable_correct; auto.
-  apply same_typ_correct; auto.
-Qed.
-
-End CORRECT_COLORING.
-
-(** * Correctness of clipping *)
-
-(** We then show the correctness of the ``clipped'' coloring
-  returned by [alloc_of_coloring] applied to a candidate coloring
-  that passes the a posteriori checks. *)
-
-Section ALLOC_OF_COLORING.
-
-Variable g: graph.
-Variable env: regenv.
-Let allregs := all_interf_regs g.
-Variable coloring: reg -> loc.
-Let alloc := alloc_of_coloring coloring env allregs.
-
-Lemma alloc_of_coloring_correct_1:
-  forall r1 r2,
-  check_coloring g env allregs coloring = true ->
-  SetRegReg.In (r1, r2) g.(interf_reg_reg) ->
-  alloc r1 <> alloc r2.
-Proof.
-  unfold check_coloring, alloc, alloc_of_coloring; intros.
-  elim (andb_prop _ _ H); intros.
-  generalize (all_interf_regs_correct_1 _ _ _ H0).
-  intros [A B].
-  unfold allregs. rewrite Regset.mem_1; auto. rewrite Regset.mem_1; auto.
-  eapply check_coloring_1_correct; eauto.
-Qed.
-
-Lemma alloc_of_coloring_correct_2:
-  forall r1 mr2,
-  check_coloring g env allregs coloring = true ->
-  SetRegMreg.In (r1, mr2) g.(interf_reg_mreg) ->
-  alloc r1 <> R mr2.
-Proof.
-  unfold check_coloring, alloc, alloc_of_coloring; intros.
-  elim (andb_prop _ _ H); intros.
-  elim (andb_prop _ _ H2); intros.
-  generalize (all_interf_regs_correct_2 _ _ _ H0). intros.
-  unfold allregs. rewrite Regset.mem_1; auto. 
-  eapply check_coloring_2_correct; eauto.
-Qed.
-
-Lemma alloc_of_coloring_correct_3:
-  forall r,
-  check_coloring g env allregs coloring = true ->
-  loc_acceptable (alloc r).
-Proof.
-  unfold check_coloring, alloc, alloc_of_coloring; intros.
-  elim (andb_prop _ _ H); intros.
-  elim (andb_prop _ _ H1); intros.
-  caseEq (Regset.mem r allregs); intro.
-  generalize (check_coloring_3_correct _ _ _ r H3 H4). tauto.
-  case (env r); simpl.
-  unfold dummy_int_reg. intuition congruence.
-  unfold dummy_float_reg. intuition congruence.
-Qed.
-
-Lemma alloc_of_coloring_correct_4:
-  forall r,
-  check_coloring g env allregs coloring = true ->
-  env r = Loc.type (alloc r).
-Proof.
-  unfold check_coloring, alloc, alloc_of_coloring; intros.
-  elim (andb_prop _ _ H); intros.
-  elim (andb_prop _ _ H1); intros.
-  caseEq (Regset.mem r allregs); intro.
-  generalize (check_coloring_3_correct _ _ _ r H3 H4). tauto.
-  case (env r); reflexivity.
-Qed.
-
-End ALLOC_OF_COLORING.
-
-(** * Correctness of the whole graph coloring algorithm *)
-
-(** Combining results from the previous sections, we now summarize
-  the correctness properties of the assignment (of locations to
-  registers) returned by [regalloc]. *)
-
-Definition correct_alloc_instr
-    (live: PMap.t Regset.t) (alloc: reg -> loc) 
-    (pc: node) (instr: instruction) : Prop :=
-  match instr with
-  | Iop op args res s =>
-      match is_move_operation op args with
-      | Some arg =>
-          forall r,
-          Regset.In res live!!pc ->
-          Regset.In r live!!pc ->
-          r <> res -> r <> arg -> alloc r <> alloc res
-      | None =>
-          forall r,
-          Regset.In res live!!pc ->
-          Regset.In r live!!pc ->
-          r <> res -> alloc r <> alloc res
-      end
-  | Iload chunk addr args res s =>
-      forall r,
-      Regset.In res live!!pc ->
-      Regset.In r live!!pc ->
-      r <> res -> alloc r <> alloc res
-  | Icall sig ros args res s =>
-      (forall r,
-        Regset.In r live!!pc ->
-        r <> res ->
-        ~(In (alloc r) destroyed_at_call))
-   /\ (forall r,
-        Regset.In r live!!pc ->
-        r <> res -> alloc r <> alloc res)
-   /\ (match ros with
-        | inl rfun => ~(In (alloc rfun) (loc_arguments sig))
-        | inr idfun => True
-        end)
-  | Itailcall sig ros args =>
-      (match ros with
-        | inl rfun => ~(In (alloc rfun) (loc_arguments sig))
-        | inr idfun => True
-        end)
-  | Ibuiltin ef args res s =>
-      forall r,
-      Regset.In r live!!pc ->
-      r <> res -> alloc r <> alloc res
-  | _ =>
-      True
-  end.
-
-Section REGALLOC_PROPERTIES.
-
-Variable f: function.
-Variable env: regenv.
-Variable live: PMap.t Regset.t.
-Variable live0: Regset.t.
-Variable alloc: reg -> loc.
-
-Let g := interf_graph f live live0.
-Let allregs := all_interf_regs g.
-Let coloring := graph_coloring f g env allregs.
-
-Lemma regalloc_ok:
-  regalloc f live live0 env = Some alloc ->
-  check_coloring g env allregs coloring = true /\
-  alloc = alloc_of_coloring coloring env allregs.
-Proof.
-  unfold regalloc, coloring, allregs, g.
-  case (check_coloring (interf_graph f live live0) env).
-  intro EQ; injection EQ; intro; clear EQ.
-  split. auto. auto.
-  intro; discriminate.
-Qed.
-
-Lemma regalloc_acceptable:
-  forall r,
-  regalloc f live live0 env = Some alloc ->
-  loc_acceptable (alloc r).
-Proof.
-  intros. elim (regalloc_ok H); intros.
-  rewrite H1. unfold allregs. apply alloc_of_coloring_correct_3.
-  exact H0.
-Qed.
-
-Lemma regsalloc_acceptable:
-  forall rl,
-  regalloc f live live0 env = Some alloc ->
-  locs_acceptable (List.map alloc rl).
-Proof.
-  intros; red; intros.
-  elim (list_in_map_inv _ _ _ H0). intros r [EQ IN].
-  subst l. apply regalloc_acceptable. auto. 
-Qed.
-
-Lemma regalloc_preserves_types:
-  forall r,
-  regalloc f live live0 env = Some alloc ->
-  Loc.type (alloc r) = env r.
-Proof.
-  intros. elim (regalloc_ok H); intros.
-  rewrite H1. unfold allregs. symmetry.
-  apply alloc_of_coloring_correct_4.
-  exact H0.
-Qed.
-
-Lemma correct_interf_alloc_instr:
-  forall pc instr,
-  (forall r1 r2, interfere r1 r2 g -> alloc r1 <> alloc r2) ->
-  (forall r1 mr2, interfere_mreg r1 mr2 g -> alloc r1 <> R mr2) ->
-  (forall r, loc_acceptable (alloc r)) ->
-  correct_interf_instr live!!pc instr g ->
-  correct_alloc_instr live alloc pc instr.
-Proof.
-  intros pc instr ALL1 ALL2 ALL3.
-  unfold correct_interf_instr, correct_alloc_instr;
-  destruct instr; auto.
-  destruct (is_move_operation o l); auto.
-  (* Icall *)
-  intros [A [B C]].
-  split. intros; red; intros. 
-  unfold destroyed_at_call in H1.
-  generalize (list_in_map_inv R _ _ H1). 
-  intros [mr [EQ IN]]. 
-  generalize (A r0 mr H IN H0). intro.
-  generalize (ALL2 _ _ H2). contradiction.
-  split. auto.
-  destruct s0; auto. red; intros.
-  generalize (ALL3 r0). generalize (loc_arguments_acceptable _ _ H).
-  unfold loc_argument_acceptable, loc_acceptable.
-  caseEq (alloc r0). intros.
-  elim (ALL2 r0 m). apply C; auto. congruence. auto. 
-  destruct s0; auto.
-  (* Itailcall *)
-  destruct s0; auto. red; intros.
-  generalize (ALL3 r). generalize (loc_arguments_acceptable _ _ H0).
-  unfold loc_argument_acceptable, loc_acceptable.
-  caseEq (alloc r). intros.
-  elim (ALL2 r m). apply H; auto. congruence. auto. 
-  destruct s0; auto.
-Qed.
-  
-Lemma regalloc_correct_1:
-  forall pc instr,
-  regalloc f live live0 env = Some alloc ->
-  f.(fn_code)!pc = Some instr ->
-  correct_alloc_instr live alloc pc instr.
-Proof.
-  intros. elim (regalloc_ok H); intros.
-  apply correct_interf_alloc_instr.
-  intros. rewrite H2. unfold allregs. red in H3. 
-  elim (ordered_pair_charact r1 r2); intro.
-  apply alloc_of_coloring_correct_1. auto. rewrite H4 in H3; auto.
-  apply sym_not_equal.
-  apply alloc_of_coloring_correct_1. auto. rewrite H4 in H3; auto.
-  intros. rewrite H2. unfold allregs.
-  apply alloc_of_coloring_correct_2. auto. exact H3.
-  intros. eapply regalloc_acceptable; eauto.
-  unfold g. apply interf_graph_correct_1. auto. 
-Qed.
-
-Lemma regalloc_correct_2:
-  regalloc f live live0 env = Some alloc ->
-  list_norepet f.(fn_params) ->
-  list_norepet (List.map alloc f.(fn_params)).
-Proof.
-  intros. elim (regalloc_ok H); intros.
-  apply list_map_norepet; auto.
-  intros. rewrite H2. unfold allregs. 
-  elim (ordered_pair_charact x y); intro.
-  apply alloc_of_coloring_correct_1. auto. 
-  change positive with reg. rewrite <- H6.
-  change (interfere x y g). unfold g. 
-  apply interf_graph_correct_2; auto.
-  apply sym_not_equal.
-  apply alloc_of_coloring_correct_1. auto. 
-  change positive with reg. rewrite <- H6.
-  change (interfere x y g). unfold g. 
-  apply interf_graph_correct_2; auto.
-Qed.
-
-Lemma regalloc_correct_3:
-  forall r1 r2,
-  regalloc f live live0 env = Some alloc ->
-  In r1 f.(fn_params) ->
-  Regset.In r2 live0 ->
-  r1 <> r2 ->
-  alloc r1 <> alloc r2.
-Proof.
-  intros. elim (regalloc_ok H); intros.
-  rewrite H4; unfold allregs.
-  elim (ordered_pair_charact r1 r2); intro.
-  apply alloc_of_coloring_correct_1. auto. 
-  change positive with reg. rewrite <- H5.
-  change (interfere r1 r2 g). unfold g.
-  apply interf_graph_correct_3; auto.
-  apply sym_not_equal.
-  apply alloc_of_coloring_correct_1. auto. 
-  change positive with reg. rewrite <- H5.
-  change (interfere r1 r2 g). unfold g.
-  apply interf_graph_correct_3; auto.
-Qed.
-
-End REGALLOC_PROPERTIES.
diff --git a/backend/InterfGraph.v b/backend/InterfGraph.v
deleted file mode 100644
index 877c7c6..0000000
--- a/backend/InterfGraph.v
+++ /dev/null
@@ -1,302 +0,0 @@
-(* *********************************************************************)
-(*                                                                     *)
-(*              The Compcert verified compiler                         *)
-(*                                                                     *)
-(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
-(*                                                                     *)
-(*  Copyright Institut National de Recherche en Informatique et en     *)
-(*  Automatique.  All rights reserved.  This file is distributed       *)
-(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
-(*                                                                     *)
-(* *********************************************************************)
-
-(** Representation of interference graphs for register allocation. *)
-
-Require Import Coqlib.
-Require Import FSets.
-Require Import FSetAVL.
-Require Import Ordered.
-Require Import Registers.
-Require Import Locations.
-
-(** Interference graphs are undirected graphs with two kinds of nodes:
-- RTL pseudo-registers;
-- Machine registers.
-
-and four kind of edges:
-- Conflict edges between two pseudo-registers.
-  (Meaning: these two pseudo-registers must not be assigned the same
-   location.)
-- Conflict edges between a pseudo-register and a machine register
-  (Meaning: this pseudo-register must not be assigned this machine
-   register.)
-- Preference edges between two pseudo-registers.
-  (Meaning: the generated code would be more efficient if those two
-   pseudo-registers were assigned the same location, but if this is not
-   possible, the generated code will still be correct.)
-- Preference edges between a pseudo-register and a machine register
-  (Meaning: the generated code would be more efficient if this
-   pseudo-register was assigned this machine register, but if this is not
-   possible, the generated code will still be correct.)
-
-A graph is represented by four finite sets of edges (one of each kind
-above).  An edge is represented by a pair of two pseudo-registers or
-a pair (pseudo-register, machine register).  
-In the case of two pseudo-registers ([r1], [r2]), we adopt the convention
-that [r1] <= [r2], so as to reflect the undirected nature of the edge.
-*)
-
-Module OrderedReg <: OrderedType with Definition t := reg := OrderedPositive.
-Module OrderedRegReg := OrderedPair(OrderedReg)(OrderedReg).
-Module OrderedMreg := OrderedIndexed(IndexedMreg).
-Module OrderedRegMreg := OrderedPair(OrderedReg)(OrderedMreg).
-
-Module SetRegReg := FSetAVL.Make(OrderedRegReg).
-Module SetRegMreg := FSetAVL.Make(OrderedRegMreg).
-
-Record graph: Type := mkgraph {
-  interf_reg_reg: SetRegReg.t;
-  interf_reg_mreg: SetRegMreg.t;
-  pref_reg_reg: SetRegReg.t;
-  pref_reg_mreg: SetRegMreg.t
-}.
-
-Definition empty_graph :=
-  mkgraph SetRegReg.empty SetRegMreg.empty
-          SetRegReg.empty SetRegMreg.empty.
-
-(** The following functions add a new edge (if not already present)
-  to the given graph. *)
-
-Definition ordered_pair (x y: reg) :=
-  if plt x y then (x, y) else (y, x).
-
-Definition add_interf (x y: reg) (g: graph) :=
-  mkgraph (SetRegReg.add (ordered_pair x y) g.(interf_reg_reg))
-          g.(interf_reg_mreg)
-          g.(pref_reg_reg)
-          g.(pref_reg_mreg).
-
-Definition add_interf_mreg  (x: reg) (y: mreg) (g: graph) :=
-  mkgraph g.(interf_reg_reg)
-          (SetRegMreg.add (x, y) g.(interf_reg_mreg))
-          g.(pref_reg_reg)
-          g.(pref_reg_mreg).
-
-Definition add_pref (x y: reg) (g: graph) :=
-  mkgraph g.(interf_reg_reg)
-          g.(interf_reg_mreg)
-          (SetRegReg.add (ordered_pair x y) g.(pref_reg_reg))
-          g.(pref_reg_mreg).
-
-Definition add_pref_mreg  (x: reg) (y: mreg) (g: graph) :=
-  mkgraph g.(interf_reg_reg)
-          g.(interf_reg_mreg)
-          g.(pref_reg_reg)
-          (SetRegMreg.add (x, y) g.(pref_reg_mreg)).
-
-(** [interfere x y g] holds iff there is a conflict edge in [g]
-  between the two pseudo-registers [x] and [y]. *)
-
-Definition interfere (x y: reg) (g: graph) : Prop :=
-  SetRegReg.In (ordered_pair x y) g.(interf_reg_reg).
-
-(** [interfere_mreg x y g] holds iff there is a conflict edge in [g]
-  between the pseudo-register [x] and the machine register [y]. *)
-
-Definition interfere_mreg (x: reg) (y: mreg) (g: graph) : Prop :=
-  SetRegMreg.In (x, y) g.(interf_reg_mreg).
-
-Lemma ordered_pair_charact:
-  forall x y,
-  ordered_pair x y = (x, y) \/ ordered_pair x y = (y, x).
-Proof.
-  unfold ordered_pair; intros.
-  case (plt x y); intro; tauto.
-Qed.
-
-Lemma ordered_pair_sym:
-  forall x y, ordered_pair y x = ordered_pair x y.
-Proof.
-  unfold ordered_pair; intros.
-  destruct (plt y x); destruct (plt x y).
-  elim (Plt_strict x). eapply Plt_trans; eauto. 
-  auto.
-  auto.
-  destruct (Pos.lt_total x y) as [A | [A | A]]. 
-  elim n0; auto.
-  congruence.
-  elim n; auto.
-Qed.
-
-Lemma interfere_sym:
-  forall x y g, interfere x y g -> interfere y x g.
-Proof.
-  unfold interfere; intros.
-  rewrite ordered_pair_sym. auto.
-Qed.
-
-(** [graph_incl g1 g2] holds if [g2] contains all the conflict edges of [g1]
-  and possibly more. *)
-
-Definition graph_incl (g1 g2: graph) : Prop :=
-  (forall x y, interfere x y g1 -> interfere x y g2) /\
-  (forall x y, interfere_mreg x y g1 -> interfere_mreg x y g2).
-
-Lemma graph_incl_trans:
-  forall g1 g2 g3, graph_incl g1 g2 -> graph_incl g2 g3 -> graph_incl g1 g3.
-Proof.
-  unfold graph_incl; intros. 
-  elim H0; elim H; intros.
-  split; eauto.
-Qed.
-
-(** We show that the [add_] functions correctly record the desired
-  conflicts, and preserve whatever conflict edges were already present. *)
-
-Lemma add_interf_correct:
-  forall x y g,
-  interfere x y (add_interf x y g).
-Proof.
-  intros. unfold interfere, add_interf; simpl.
-  apply SetRegReg.add_1. auto. 
-Qed.
-
-Lemma add_interf_incl:
-  forall a b g,  graph_incl g (add_interf a b g).
-Proof.
-  intros. split; intros.
-  unfold add_interf, interfere; simpl.
-  apply SetRegReg.add_2. exact H.
-  exact H.
-Qed.
-
-Lemma add_interf_mreg_correct:
-  forall x y g,
-  interfere_mreg x y (add_interf_mreg x y g).
-Proof.
-  intros. unfold interfere_mreg, add_interf_mreg; simpl.
-  apply SetRegMreg.add_1. auto. 
-Qed.
-
-Lemma add_interf_mreg_incl:
-  forall a b g,  graph_incl g (add_interf_mreg a b g).
-Proof.
-  intros. split; intros.
-  exact H.
-  unfold add_interf_mreg, interfere_mreg; simpl.
-  apply SetRegMreg.add_2. exact H.
-Qed.
-
-Lemma add_pref_incl:
-  forall a b g,  graph_incl g (add_pref a b g).
-Proof.
-  intros. split; intros.
-  exact H.
-  exact H.
-Qed.
-
-Lemma add_pref_mreg_incl:
-  forall a b g,  graph_incl g (add_pref_mreg a b g).
-Proof.
-  intros. split; intros.
-  exact H.
-  exact H.
-Qed.
-
-(** [all_interf_regs g] returns the set of pseudo-registers that
-  are nodes of [g]. *)
-
-Definition add_intf2 (r1r2: reg * reg) (u: Regset.t) : Regset.t :=
-  Regset.add (fst r1r2) (Regset.add (snd r1r2) u).
-Definition add_intf1 (r1m2: reg * mreg) (u: Regset.t) : Regset.t :=
-  Regset.add (fst r1m2) u.
-
-Definition all_interf_regs (g: graph) : Regset.t :=
-  let s1 := SetRegMreg.fold add_intf1 g.(interf_reg_mreg) Regset.empty in
-  let s2 := SetRegMreg.fold add_intf1 g.(pref_reg_mreg) s1 in
-  let s3 := SetRegReg.fold add_intf2 g.(interf_reg_reg) s2 in
-  SetRegReg.fold add_intf2 g.(pref_reg_reg) s3.
-
-Lemma in_setregreg_fold:
-  forall g r1 r2 u,
-  SetRegReg.In (r1, r2) g \/ Regset.In r1 u /\ Regset.In r2 u ->
-  Regset.In r1 (SetRegReg.fold add_intf2 g u) /\
-  Regset.In r2 (SetRegReg.fold add_intf2 g u).
-Proof.
-  set (add_intf2' := fun u r1r2 => add_intf2 r1r2 u).
-  assert (forall l r1 r2 u,
-    InA OrderedRegReg.eq (r1,r2) l \/ Regset.In r1 u /\ Regset.In r2 u ->
-    Regset.In r1 (List.fold_left add_intf2' l u) /\
-    Regset.In r2 (List.fold_left add_intf2' l u)).
-  induction l; intros; simpl.
-  elim H; intro. inversion H0. auto.
-  apply IHl. destruct a as [a1 a2].
-  elim H; intro. inversion H0; subst. 
-  red in H2. simpl in H2. destruct H2. subst r1 r2.
-  right; unfold add_intf2', add_intf2; simpl; split.
-  apply Regset.add_1. auto. 
-  apply Regset.add_2. apply Regset.add_1. auto. 
-  tauto.
-  right; unfold add_intf2', add_intf2; simpl; split;
-  apply Regset.add_2; apply Regset.add_2; tauto.
-
-  intros. rewrite SetRegReg.fold_1. apply H. 
-  intuition. 
-Qed.
-
-Lemma in_setregreg_fold':
-  forall g r u,
-  Regset.In r u ->
-  Regset.In r (SetRegReg.fold add_intf2 g u).
-Proof.
-  intros. exploit in_setregreg_fold. eauto. 
-  intros [A B]. eauto.
-Qed.
-
-Lemma in_setregmreg_fold:
-  forall g r1 mr2 u,
-  SetRegMreg.In (r1, mr2) g \/ Regset.In r1 u ->
-  Regset.In r1 (SetRegMreg.fold add_intf1 g u).
-Proof.
-  set (add_intf1' := fun u r1mr2 => add_intf1 r1mr2 u).
-  assert (forall l r1 mr2 u,
-    InA OrderedRegMreg.eq (r1,mr2) l \/ Regset.In r1 u ->
-    Regset.In r1 (List.fold_left add_intf1' l u)).
-  induction l; intros; simpl.
-  elim H; intro. inversion H0. auto.
-  apply IHl with mr2. destruct a as [a1 a2].
-  elim H; intro. inversion H0; subst. 
-  red in H2. simpl in H2. destruct H2. subst r1 mr2.
-  right; unfold add_intf1', add_intf1; simpl.
-  apply Regset.add_1; auto.
-  tauto.
-  right; unfold add_intf1', add_intf1; simpl.
-  apply Regset.add_2; auto.
-
-  intros. rewrite SetRegMreg.fold_1. apply H with mr2. 
-  intuition.
-Qed.
-
-Lemma all_interf_regs_correct_1:
-  forall r1 r2 g,
-  SetRegReg.In (r1, r2) g.(interf_reg_reg) ->
-  Regset.In r1 (all_interf_regs g) /\
-  Regset.In r2 (all_interf_regs g).
-Proof.
-  intros. unfold all_interf_regs. 
-  apply in_setregreg_fold. right.
-  apply in_setregreg_fold. tauto.
-Qed.
-
-Lemma all_interf_regs_correct_2:
-  forall r1 mr2 g,
-  SetRegMreg.In (r1, mr2) g.(interf_reg_mreg) ->
-  Regset.In r1 (all_interf_regs g).
-Proof.
-  intros. unfold all_interf_regs.
-  apply in_setregreg_fold'. apply in_setregreg_fold'. 
-  apply in_setregmreg_fold with mr2. right. 
-  apply in_setregmreg_fold with mr2. eauto.
-Qed.
-
diff --git a/backend/Parallelmove.v b/backend/Parallelmove.v
deleted file mode 100644
index 4930ccd..0000000
--- a/backend/Parallelmove.v
+++ /dev/null
@@ -1,365 +0,0 @@
-(* *********************************************************************)
-(*                                                                     *)
-(*              The Compcert verified compiler                         *)
-(*                                                                     *)
-(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
-(*                                                                     *)
-(*  Copyright Institut National de Recherche en Informatique et en     *)
-(*  Automatique.  All rights reserved.  This file is distributed       *)
-(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
-(*                                                                     *)
-(* *********************************************************************)
-
-(** Translation of parallel moves into sequences of individual moves.
-
-  In this file, we adapt the generic "parallel move" algorithm
-  (developed and proved correct in module [Parmov]) to the idiosyncraties
-  of the [LTLin] and [Linear] intermediate languages.  While the generic
-  algorithm assumes that registers never overlap, the locations
-  used in [LTLin] and [Linear] can overlap, and assigning one location
-  can set the values of other, overlapping locations to [Vundef].
-  We address this issue in the remainder of this file.
-*)
-
-Require Import Coqlib.
-Require Parmov.
-Require Import Values.
-Require Import AST.
-Require Import Locations.
-Require Import Conventions.
-
-(** * Instantiating the generic parallel move algorithm *)
-
-(** The temporary location to use for a move is determined
-  by the type of the data being moved: register [IT2] for an
-  integer datum, and register [FT2] for a floating-point datum. *)
-
-Definition temp_for (l: loc) : loc :=
-  match Loc.type l with Tint => R IT2 | Tfloat => R FT2 end.
-
-Definition parmove (srcs dsts: list loc) :=
-  Parmov.parmove2 loc Loc.eq temp_for srcs dsts.
-
-Definition moves := (list (loc * loc))%type.
-
-(** [exec_seq m] gives semantics to a sequence of elementary moves.
-  This semantics ignores the possibility of overlap: only the
-  target locations are updated, but the locations they
-  overlap with are not set to [Vundef].  See [effect_seqmove] below
-  for a semantics that accounts for overlaps. *)
-
-Definition exec_seq (m: moves) (e: Locmap.t) : Locmap.t :=
-  Parmov.exec_seq loc Loc.eq val m e.
-  
-Lemma temp_for_charact:
-  forall l, temp_for l = R IT2 \/ temp_for l = R FT2.
-Proof.
-  intro; unfold temp_for. destruct (Loc.type l); tauto.
-Qed.
-
-Lemma is_not_temp_charact:
-  forall l,
-  Parmov.is_not_temp loc temp_for l <-> l <> R IT2 /\ l <> R FT2.
-Proof.
-  intros. unfold Parmov.is_not_temp. 
-  destruct (Loc.eq l (R IT2)). 
-  subst l. intuition. apply (H (R IT2)). reflexivity. discriminate.
-  destruct (Loc.eq l (R FT2)).
-  subst l. intuition. apply (H (R FT2)). reflexivity. 
-  assert (forall d, l <> temp_for d). 
-    intro. elim (temp_for_charact d); congruence.
-  intuition. 
-Qed.
-
-Lemma disjoint_temp_not_temp:
-  forall l, Loc.notin l temporaries -> Parmov.is_not_temp loc temp_for l.
-Proof.
-  intros. rewrite is_not_temp_charact. 
-  unfold temporaries in H; simpl in H. 
-  split; apply Loc.diff_not_eq; tauto.
-Qed.
-
-Lemma loc_norepet_norepet:
-  forall l, Loc.norepet l -> list_norepet l.
-Proof.
-  induction 1; constructor. 
-  apply Loc.notin_not_in; auto. auto.
-Qed.
-
-(** Instantiating the theorems proved in [Parmov], we obtain
-  the following properties of semantic correctness and well-typedness
-  of the generated sequence of moves.  Note that the semantic
-  correctness result is stated in terms of the [exec_seq] semantics,
-  and therefore does not account for overlap between locations. *)
-
-Lemma parmove_prop_1:
-  forall srcs dsts,
-  List.length srcs = List.length dsts ->
-  Loc.norepet dsts ->
-  Loc.disjoint srcs temporaries ->
-  Loc.disjoint dsts temporaries ->
-  forall e,
-  let e' := exec_seq (parmove srcs dsts) e in
-  List.map e' dsts = List.map e srcs /\
-  forall l, ~In l dsts -> l <> R IT2 -> l <> R FT2 -> e' l = e l.
-Proof.
-  intros. 
-  assert (NR: list_norepet dsts) by (apply loc_norepet_norepet; auto).
-  assert (NTS: forall r, In r srcs -> Parmov.is_not_temp loc temp_for r).
-    intros. apply disjoint_temp_not_temp. apply Loc.disjoint_notin with srcs; auto.
-  assert (NTD: forall r, In r dsts -> Parmov.is_not_temp loc temp_for r).
-    intros. apply disjoint_temp_not_temp. apply Loc.disjoint_notin with dsts; auto.
-  generalize (Parmov.parmove2_correctness loc Loc.eq temp_for val srcs dsts H NR NTS NTD e).
-  change (Parmov.exec_seq loc Loc.eq val (Parmov.parmove2 loc Loc.eq temp_for srcs dsts) e) with e'.
-  intros [A B].
-  split. auto. intros. apply B. auto. rewrite is_not_temp_charact; auto.
-Qed.
-
-Lemma parmove_prop_2:
-  forall srcs dsts s d,
-  In (s, d) (parmove srcs dsts) ->
-     (In s srcs \/ s = R IT2 \/ s = R FT2)
-  /\ (In d dsts \/ d = R IT2 \/ d = R FT2).
-Proof.
-  intros srcs dsts.
-  set (mu := List.combine srcs dsts).
-  assert (forall s d, Parmov.wf_move loc temp_for mu s d ->
-            (In s srcs \/ s = R IT2 \/ s = R FT2)
-         /\ (In d dsts \/ d = R IT2 \/ d = R FT2)).
-  unfold mu; induction 1. 
-  split. 
-    left. eapply List.in_combine_l; eauto.
-    left. eapply List.in_combine_r; eauto.
-  split. 
-    right. apply temp_for_charact. 
-    tauto.
-  split.
-    tauto.
-    right. apply temp_for_charact.
-  intros. apply H. 
-  apply (Parmov.parmove2_wf_moves loc Loc.eq temp_for srcs dsts s d H0). 
-Qed.
-
-Lemma loc_type_temp_for:
-  forall l, Loc.type (temp_for l) = Loc.type l.
-Proof.
-  intros; unfold temp_for. destruct (Loc.type l); reflexivity. 
-Qed.
-
-Lemma loc_type_combine:
-  forall srcs dsts,
-  List.map Loc.type srcs = List.map Loc.type dsts ->
-  forall s d,
-  In (s, d) (List.combine srcs dsts) ->
-  Loc.type s = Loc.type d.
-Proof.
-  induction srcs; destruct dsts; simpl; intros; try discriminate.
-  elim H0.
-  elim H0; intros. inversion H1; subst. congruence.
-  apply IHsrcs with dsts. congruence. auto.
-Qed.
-
-Lemma parmove_prop_3:
-  forall srcs dsts,
-  List.map Loc.type srcs = List.map Loc.type dsts ->
-  forall s d,
-  In (s, d) (parmove srcs dsts) -> Loc.type s = Loc.type d.
-Proof.
-  intros srcs dsts TYP.
-  set (mu := List.combine srcs dsts).
-  assert (forall s d, Parmov.wf_move loc temp_for mu s d ->
-            Loc.type s = Loc.type d).
-  unfold mu; induction 1. 
-  eapply loc_type_combine; eauto.
-  rewrite loc_type_temp_for; auto.
-  rewrite loc_type_temp_for; auto.
-  intros. apply H. 
-  apply (Parmov.parmove2_wf_moves loc Loc.eq temp_for srcs dsts s d H0). 
-Qed.
-
-(** * Accounting for overlap between locations *)
-
-Section EQUIVALENCE.
-
-(** We now prove the correctness of the generated sequence of elementary
-  moves, accounting for possible overlap between locations.
-  The proof is conducted under the following hypotheses: there must
-  be no partial overlap between
-- two distinct destinations (hypothesis [NOREPET]);
-- a source location and a destination location (hypothesis [NO_OVERLAP]).
-*)
-
-Variables srcs dsts: list loc.
-Hypothesis LENGTH: List.length srcs = List.length dsts.
-Hypothesis NOREPET: Loc.norepet dsts.
-Hypothesis NO_OVERLAP: Loc.no_overlap srcs dsts.
-Hypothesis NO_SRCS_TEMP: Loc.disjoint srcs temporaries.
-Hypothesis NO_DSTS_TEMP: Loc.disjoint dsts temporaries.
-
-(** [no_overlap_dests l] holds if location [l] does not partially overlap
-  a destination location: either it is identical to one of the
-  destinations, or it is disjoint from all destinations. *)
-
-Definition no_overlap_dests (l: loc) : Prop :=
-  forall d, In d dsts -> l = d \/ Loc.diff l d.
-
-(** We show that [no_overlap_dests] holds for any destination location
-  and for any source location. *)
-
-Lemma dests_no_overlap_dests:
-  forall l, In l dsts -> no_overlap_dests l.
-Proof.
-  assert (forall d, Loc.norepet d ->
-          forall l1 l2, In l1 d -> In l2 d -> l1 = l2 \/ Loc.diff l1 l2).
-  induction 1; simpl; intros.
-  contradiction.
-  elim H1; intro; elim H2; intro.
-  left; congruence.
-  right. subst l1. eapply Loc.in_notin_diff; eauto.
-  right. subst l2. apply Loc.diff_sym. eapply Loc.in_notin_diff; eauto.
-  eauto.
-  intros; red; intros. eauto. 
-Qed.
-
-Lemma notin_dests_no_overlap_dests:
-  forall l, Loc.notin l dsts -> no_overlap_dests l.
-Proof.
-  intros; red; intros.
-  right. eapply Loc.in_notin_diff; eauto.
-Qed.
-
-Lemma source_no_overlap_dests:
-  forall s, In s srcs \/ s = R IT2 \/ s = R FT2 -> no_overlap_dests s.
-Proof.
-  intros. elim H; intro. exact (NO_OVERLAP s H0). 
-  elim H0; intro; subst s; red; intros;
-  right; apply Loc.diff_sym; apply NO_DSTS_TEMP; auto; simpl; tauto.
-Qed.
-
-Lemma source_not_temp1:
-  forall s, In s srcs \/ s = R IT2 \/ s = R FT2 -> 
-  Loc.diff s (R IT1) /\ Loc.diff s (R FT1) /\ Loc.notin s destroyed_at_move.
-Proof.
-  intros. destruct H.
-  exploit Loc.disjoint_notin. eexact NO_SRCS_TEMP. eauto. 
-  simpl; tauto.
-  destruct H; subst s; simpl; intuition congruence.
-Qed.
-
-Lemma dest_noteq_diff:
-  forall d l, 
-  In d dsts \/ d = R IT2 \/ d = R FT2 ->
-  l <> d ->
-  no_overlap_dests l ->
-  Loc.diff l d.
-Proof.
-  intros. elim H; intro.
-  elim (H1 d H2); intro. congruence. auto.
-  assert (forall r, l <> R r -> Loc.diff l (R r)).
-    intros. destruct l; simpl. congruence. destruct s; auto.
-  elim H2; intro; subst d; auto.
-Qed.
-
-(** [locmap_equiv e1 e2] holds if the location maps [e1] and [e2]
-  assign the same values to all locations except temporaries [IT1], [FT1]
-  and except locations that partially overlap a destination. *)
-
-Definition locmap_equiv (e1 e2: Locmap.t): Prop :=
-  forall l,
-  no_overlap_dests l -> Loc.diff l (R IT1) -> Loc.diff l (R FT1) -> Loc.notin l destroyed_at_move -> e2 l = e1 l.
-
-(** The following predicates characterize the effect of one move
-  move ([effect_move]) and of a sequence of elementary moves
-  ([effect_seqmove]).  We allow the code generated for one move
-  to use the temporaries [IT1] and [FT1] and [destroyed_at_move] in any way it needs. *)
-
-Definition effect_move (src dst: loc) (e e': Locmap.t): Prop :=
-  e' dst = e src /\
-  forall l, Loc.diff l dst -> Loc.diff l (R IT1) -> Loc.diff l (R FT1) -> Loc.notin l destroyed_at_move -> e' l = e l.
-
-Inductive effect_seqmove: list (loc * loc) -> Locmap.t -> Locmap.t -> Prop :=
-  | effect_seqmove_nil: forall e,
-      effect_seqmove nil e e
-  | effect_seqmove_cons: forall s d m e1 e2 e3,
-      effect_move s d e1 e2 ->
-      effect_seqmove m e2 e3 ->
-      effect_seqmove ((s, d) :: m) e1 e3.
-
-(** The following crucial lemma shows that [locmap_equiv] is preserved
-  by executing one move [d <- s], once using the [effect_move]
-  predicate that accounts for partial overlap and the use of
-  temporaries [IT1], [FT1], or via the [Parmov.update] function that
-  does not account for any of these. *)
-
-Lemma effect_move_equiv:
-  forall s d e1 e2 e1',
-  (In s srcs \/ s = R IT2 \/ s = R FT2) ->
-  (In d dsts \/ d = R IT2 \/ d = R FT2) ->
-  locmap_equiv e1 e2 -> effect_move s d e1 e1' ->
-  locmap_equiv e1' (Parmov.update loc Loc.eq val d (e2 s) e2).
-Proof.
-  intros. destruct H2. red; intros. 
-  unfold Parmov.update. destruct (Loc.eq l d). 
-  subst l. destruct (source_not_temp1 _ H) as [A [B C]]. 
-  rewrite H2. apply H1; auto. apply source_no_overlap_dests; auto.
-  rewrite H3; auto. apply dest_noteq_diff; auto. 
-Qed.
-
-(** We then extend the previous lemma to a sequence [mu] of elementary moves.
-*)
-
-Lemma effect_seqmove_equiv:
-  forall mu e1 e1',
-  effect_seqmove mu e1 e1' ->
-  forall e2,
-  (forall s d, In (s, d) mu ->
-     (In s srcs \/ s = R IT2 \/ s = R FT2) /\
-     (In d dsts \/ d = R IT2 \/ d = R FT2)) ->
-  locmap_equiv e1 e2 ->
-  locmap_equiv e1' (exec_seq mu e2).
-Proof.
-  induction 1; intros.
-  simpl. auto.
-  simpl. apply IHeffect_seqmove. 
-  intros. apply H1. apply in_cons; auto. 
-  destruct (H1 s d (in_eq _ _)).
-  eapply effect_move_equiv; eauto. 
-Qed.
-
-(** Here is the main result in this file: executing the sequence
-  of moves returned by the [parmove] function results in the
-  desired state for locations: the final values of destination locations
-  are the initial values of source locations, and all locations
-  that are disjoint from the temporaries and the destinations
-  keep their initial values. *)
-
-Lemma effect_parmove:
-  forall e e',
-  effect_seqmove (parmove srcs dsts) e e' ->
-  List.map e' dsts = List.map e srcs /\
-  forall l, Loc.notin l dsts -> Loc.notin l temporaries -> e' l = e l.
-Proof.
-  set (mu := parmove srcs dsts). intros.
-  assert (locmap_equiv e e) by (red; auto).
-  generalize (effect_seqmove_equiv mu e e' H e (parmove_prop_2 srcs dsts) H0).
-  intro. 
-  generalize (parmove_prop_1 srcs dsts LENGTH NOREPET NO_SRCS_TEMP NO_DSTS_TEMP e).
-  fold mu. intros [A B]. 
-  (* e' dsts = e srcs *)
-  split. rewrite <- A. apply list_map_exten; intros.
-  exploit Loc.disjoint_notin. eexact NO_DSTS_TEMP. eauto. simpl; intros.
-  apply H1. apply dests_no_overlap_dests; auto.
-  tauto. tauto. simpl; tauto. 
-  (* other locations *)
-  intros. transitivity (exec_seq mu e l). 
-  symmetry. apply H1. apply notin_dests_no_overlap_dests; auto.
-  eapply Loc.in_notin_diff; eauto. simpl; tauto.
-  eapply Loc.in_notin_diff; eauto. simpl; tauto.
-  simpl in H3; simpl; tauto.
-  apply B. apply Loc.notin_not_in; auto.
-  apply Loc.diff_not_eq. eapply Loc.in_notin_diff; eauto. simpl; tauto.
-  apply Loc.diff_not_eq. eapply Loc.in_notin_diff; eauto. simpl; tauto.
-Qed.
-
-End EQUIVALENCE.
-