1 files changed, 0 insertions, 28 deletions
diff --git a/src/Compilers/Z/MapCastByDeBruijn.v b/src/Compilers/Z/MapCastByDeBruijn.v
deleted file mode 100644
index 1985653d4..000000000
--- a/src/Compilers/Z/MapCastByDeBruijn.v
+++ /dev/null
@@ -1,28 +0,0 @@
-Require Import Coq.ZArith.ZArith.
-Require Import Crypto.Compilers.Syntax.
-Require Import Crypto.Compilers.SmartMap.
-Require Import Crypto.Compilers.MapCastByDeBruijn.
-Require Import Crypto.Compilers.Z.Syntax.
-
-Section language.
-  Context {interp_base_type_bounds : base_type -> Type}
-          (interp_op_bounds : forall src dst, op src dst -> interp_flat_type interp_base_type_bounds src -> interp_flat_type interp_base_type_bounds dst)
-          (pick_typeb : forall t, interp_base_type_bounds t -> base_type).
-  Local Notation pick_type v := (SmartFlatTypeMap pick_typeb v).
-  Context (cast_op : forall t tR (opc : op t tR) args_bs,
-              op (pick_type args_bs) (pick_type (interp_op_bounds t tR opc args_bs))).
-  Context {t : type base_type}.
-
-  Definition MapCastCompile := @MapCastCompile base_type op t.
-  Definition MapCastDoCast
-    := @MapCastDoCast
-         base_type op base_type_beq internal_base_type_dec_bl
-         interp_base_type_bounds interp_op_bounds pick_typeb cast_op t.
-  Definition MapCastDoInterp
-    := @MapCastDoInterp
-         base_type op base_type_beq internal_base_type_dec_bl
-         (fun _ t => Op (OpConst 0%Z) TT)
-         interp_base_type_bounds pick_typeb t.
-  Definition MapCast e input_bounds
-    := MapCastDoInterp input_bounds (MapCastDoCast input_bounds (MapCastCompile e)).
-End language.