1 files changed, 0 insertions, 30 deletions
diff --git a/src/Compilers/Map.v b/src/Compilers/Map.v
deleted file mode 100644
index 9fe9f7011..000000000
--- a/src/Compilers/Map.v
+++ /dev/null
@@ -1,30 +0,0 @@
-Require Import Crypto.Compilers.Syntax.
-
-Section language.
-  Context {base_type_code : Type}
-          {op : flat_type base_type_code -> flat_type base_type_code -> Type}
-          {var1 var2 : base_type_code -> Type}
-          (fvar12 : forall t, var1 t -> var2 t)
-          (fvar21 : forall t, var2 t -> var1 t).
-  Local Notation exprf := (@exprf base_type_code op).
-  Fixpoint mapf_interp_flat_type {t} (e : interp_flat_type var2 t) {struct t}
-    : interp_flat_type var1 t
-    := match t return interp_flat_type _ t -> interp_flat_type _ t with
-       | Tbase _ => fvar21 _
-       | Unit => fun v : unit => v
-       | Prod x y => fun xy => (@mapf_interp_flat_type _ (fst xy),
-                                @mapf_interp_flat_type _ (snd xy))
-       end e.
-
-  Fixpoint mapf {t} (e : @exprf var1 t) : @exprf var2 t
-    := match e in Syntax.exprf _ _ t return exprf t with
-       | TT => TT
-       | Var _ x => Var (fvar12 _ x)
-       | Op _ _ op args => Op op (@mapf _ args)
-       | LetIn _ ex _ eC => LetIn (@mapf _ ex) (fun x => @mapf _ (eC (mapf_interp_flat_type x)))
-       | Pair _ ex _ ey => Pair (@mapf _ ex) (@mapf _ ey)
-       end.
-End language.
-
-Global Arguments mapf_interp_flat_type {_ _ _} _ {t} _.
-Global Arguments mapf {_ _ _ _} _ _ {t} _.