1 files changed, 0 insertions, 41 deletions
diff --git a/src/Compilers/Named/WfInterp.v b/src/Compilers/Named/WfInterp.v
deleted file mode 100644
index e9cd8737c..000000000
--- a/src/Compilers/Named/WfInterp.v
+++ /dev/null
@@ -1,41 +0,0 @@
-Require Import Crypto.Compilers.Syntax.
-Require Import Crypto.Compilers.Named.Context.
-Require Import Crypto.Compilers.Named.Syntax.
-Require Import Crypto.Compilers.Named.Wf.
-Require Import Crypto.Util.PointedProp.
-Require Import Crypto.Util.Tactics.BreakMatch.
-Require Import Crypto.Util.Tactics.SpecializeBy.
-Require Import Crypto.Util.Tactics.DestructHead.
-
-Section language.
-  Context {base_type_code Name interp_base_type}
-          {op : flat_type base_type_code -> flat_type base_type_code -> Type}
-          {interp_op : forall src dst, op src dst -> interp_flat_type interp_base_type src -> interp_flat_type interp_base_type dst}
-          {Context : @Context base_type_code Name interp_base_type}.
-
-  Lemma wff_interpf_not_None {ctx : Context} {t} {e : @exprf base_type_code op Name t}
-        (Hwf : prop_of_option (wff ctx e))
-    : @interpf base_type_code interp_base_type op Name Context interp_op t ctx e <> None.
-  Proof using Type.
-    revert dependent ctx; induction e;
-      repeat first [ progress intros
-                   | progress simpl in *
-                   | progress unfold option_map, LetIn.Let_In in *
-                   | congruence
-                   | progress specialize_by_assumption
-                   | progress destruct_head' and
-                   | progress break_innermost_match_step
-                   | progress break_match_hyps
-                   | progress autorewrite with push_prop_of_option in *
-                   | progress specialize_by auto
-                   | solve [ intuition eauto ] ].
-  Qed.
-
-  Lemma wf_interp_not_None {ctx : Context} {t} {e : @expr base_type_code op Name t}
-        (Hwf : wf ctx e)
-        v
-    : @interp base_type_code interp_base_type op Name Context interp_op t ctx e v <> None.
-  Proof using Type.
-    destruct e; unfold interp, wf in *; apply wff_interpf_not_None; auto.
-  Qed.
-End language.