1 files changed, 0 insertions, 108 deletions
diff --git a/backend/Machtyping.v b/backend/Machtyping.v
deleted file mode 100644
index 2dc19be..0000000
--- a/backend/Machtyping.v
+++ /dev/null
@@ -1,108 +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.     *)
-(*                                                                     *)
-(* *********************************************************************)
-
-(** Type system for the Mach intermediate language. *)
-
-Require Import Coqlib.
-Require Import AST.
-Require Import Integers.
-Require Import Op.
-Require Import Locations.
-Require Import Conventions.
-Require Import Mach.
-
-(** * Typing rules *)
-
-Inductive wt_instr : instruction -> Prop :=
-  | wt_Mlabel:
-     forall lbl,
-     wt_instr (Mlabel lbl)
-  | wt_Mgetstack:
-     forall ofs ty r,
-     mreg_type r = ty ->
-     wt_instr (Mgetstack ofs ty r)
-  | wt_Msetstack:
-     forall ofs ty r,
-     mreg_type r = ty ->
-     wt_instr (Msetstack r ofs ty)
-  | wt_Mgetparam:
-     forall ofs ty r,
-     mreg_type r = ty ->
-     wt_instr (Mgetparam ofs ty r)
-  | wt_Mopmove:
-     forall r1 r,
-     mreg_type r1 = mreg_type r ->
-     wt_instr (Mop Omove (r1 :: nil) r)
-  | wt_Mop:
-     forall op args res,
-      op <> Omove ->
-      (List.map mreg_type args, mreg_type res) = type_of_operation op ->
-      wt_instr (Mop op args res)
-  | wt_Mload:
-      forall chunk addr args dst,
-      List.map mreg_type args = type_of_addressing addr ->
-      mreg_type dst = type_of_chunk chunk ->
-      wt_instr (Mload chunk addr args dst)
-  | wt_Mstore:
-      forall chunk addr args src,
-      List.map mreg_type args = type_of_addressing addr ->
-      mreg_type src = type_of_chunk chunk ->
-      wt_instr (Mstore chunk addr args src)
-  | wt_Mcall:
-      forall sig ros,
-      match ros with inl r => mreg_type r = Tint | inr s => True end ->
-      wt_instr (Mcall sig ros)
-  | wt_Mtailcall:
-      forall sig ros,
-      tailcall_possible sig ->
-      match ros with inl r => mreg_type r = Tint | inr s => True end ->
-      wt_instr (Mtailcall sig ros)
-  | wt_Mbuiltin:
-     forall ef args res,
-      List.map mreg_type args = (ef_sig ef).(sig_args) ->
-      mreg_type res = proj_sig_res (ef_sig ef) ->
-      wt_instr (Mbuiltin ef args res)
-  | wt_Mannot:
-      forall ef args,
-      ef_reloads ef = false ->
-      wt_instr (Mannot ef args)
-  | wt_Mgoto:
-      forall lbl,
-      wt_instr (Mgoto lbl)
-  | wt_Mcond:
-      forall cond args lbl,
-      List.map mreg_type args = type_of_condition cond ->
-      wt_instr (Mcond cond args lbl)
-  | wt_Mjumptable:
-      forall arg tbl,
-      mreg_type arg = Tint ->
-      list_length_z tbl * 4 <= Int.max_unsigned ->
-      wt_instr (Mjumptable arg tbl)
-  | wt_Mreturn: 
-      wt_instr Mreturn.
-
-Record wt_function (f: function) : Prop := mk_wt_function {
-  wt_function_instrs:
-    forall instr, In instr f.(fn_code) -> wt_instr instr;
-  wt_function_stacksize:
-    0 <= f.(fn_stacksize) <= Int.max_unsigned
-}.
-
-Inductive wt_fundef: fundef -> Prop :=
-  | wt_fundef_external: forall ef,
-      wt_fundef (External ef)
-  | wt_function_internal: forall f,
-      wt_function f ->
-      wt_fundef (Internal f).
-
-Definition wt_program (p: program) : Prop :=
-  forall i f, In (i, Gfun f) (prog_defs p) -> wt_fundef f.