1 files changed, 0 insertions, 110 deletions
diff --git a/backend/RREtyping.v b/backend/RREtyping.v
deleted file mode 100644
index 170d8ad..0000000
--- a/backend/RREtyping.v
+++ /dev/null
@@ -1,110 +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.     *)
-(*                                                                     *)
-(* *********************************************************************)
-
-(** Proof of type preservation for the [RRE] pass. *)
-
-Require Import Coqlib.
-Require Import AST.
-Require Import Locations.
-Require Import Linear.
-Require Import Lineartyping.
-Require Import Conventions.
-Require Import RRE.
-Require Import RREproof.
-
-Remark wt_cons:
-  forall f c i, wt_instr f i -> wt_code f c -> wt_code f (i::c).
-Proof.
-  intros; red; intros. simpl in H1; destruct H1. congruence. auto.
-Qed.
-
-Hint Constructors wt_instr : linearty.
-Hint Resolve wt_cons: linearty.
-
-Definition wt_eqs (eqs: equations) :=
-  forall e, In e eqs -> slot_type (e_slot e) = mreg_type (e_reg e).
-
-Lemma wt_eqs_nil:
-  wt_eqs nil.
-Proof. red; simpl; tauto. Qed.
-
-Lemma wt_eqs_cons:
-  forall r s eqs,
-  slot_type s = mreg_type r -> wt_eqs eqs -> wt_eqs (mkeq r s :: eqs).
-Proof.
-  intros; red; simpl; intros. destruct H1. subst; simpl; auto. auto.
-Qed.
-  
-Lemma wt_kill_loc:
-  forall l eqs,
-  wt_eqs eqs -> wt_eqs (kill_loc l eqs).
-Proof.
-  intros; red; intros. exploit In_kill_loc; eauto. intros [A B]. auto.
-Qed.
-
-Lemma wt_kill_locs:
-  forall ll eqs,
-  wt_eqs eqs -> wt_eqs (kill_locs ll eqs).
-Proof.
-  intros; red; intros. exploit In_kill_locs; eauto. intros [A B]. auto.
-Qed.
-
-Lemma wt_kill_temps:
-  forall eqs, wt_eqs eqs -> wt_eqs (kill_temps eqs).
-Proof.
-  exact (wt_kill_locs temporaries).
-Qed.
-
-Lemma wt_kill_at_move:
-  forall eqs, wt_eqs eqs -> wt_eqs (kill_at_move eqs).
-Proof.
-  exact (wt_kill_locs destroyed_at_move).
-Qed.
-
-Hint Resolve wt_eqs_nil wt_eqs_cons wt_kill_loc wt_kill_locs
-             wt_kill_temps wt_kill_at_move: linearty.
-
-Lemma wt_kill_op:
-  forall op eqs, wt_eqs eqs -> wt_eqs (kill_op op eqs).
-Proof.
-  intros; destruct op; simpl; apply wt_kill_locs; auto.
-Qed.
-
-Hint Resolve wt_kill_op: linearty.
-
-Lemma wt_transf_code:
-  forall f c eqs, wt_code f c -> wt_eqs eqs ->
-  wt_code (transf_function f) (transf_code eqs c nil).
-Proof.
-  induction c; intros; simpl.
-  red; simpl; tauto.
-  assert (WI: wt_instr f a) by auto with coqlib.
-  assert (WC: wt_code f c) by (red; auto with coqlib).
-  clear H.
-  inv WI; rewrite ? transf_code_eq; auto 10 with linearty.
-  destruct (is_incoming s) eqn:?. auto with linearty.
-  destruct (contains_equation s r eqs). auto with linearty.
-  destruct (find_reg_containing s eqs) as [r'|] eqn:?; auto with linearty.
-  assert (mreg_type r' = mreg_type r).
-  exploit H0. eapply find_reg_containing_sound; eauto. simpl. congruence.
-  rewrite ! transf_code_eq.
-  destruct (safe_move_insertion c); auto 10 with linearty.
-Qed.
-
-Lemma program_typing_preserved:
-  forall p, wt_program p -> wt_program (transf_program p).
-Proof.
-  intros. red; intros. exploit transform_program_function; eauto. 
-  intros [f0 [A B]]. subst f. exploit H; eauto. intros WTFD.
-  inv WTFD; simpl; constructor.  red; simpl. 
-  apply wt_transf_code; auto with linearty.
-Qed.