1 files changed, 0 insertions, 45 deletions
diff --git a/src/Compilers/Named/InterpSideConditionsInterp.v b/src/Compilers/Named/InterpSideConditionsInterp.v
deleted file mode 100644
index 72bb9c9e0..000000000
--- a/src/Compilers/Named/InterpSideConditionsInterp.v
+++ /dev/null
@@ -1,45 +0,0 @@
-Require Import Crypto.Compilers.Syntax.
-Require Import Crypto.Compilers.Named.Syntax.
-Require Import Crypto.Compilers.Named.Context.
-Require Import Crypto.Compilers.Named.InterpSideConditions.
-Require Import Crypto.Util.PointedProp.
-Require Import Crypto.Util.Notations.
-Require Import Crypto.Util.Tactics.BreakMatch.
-Require Import Crypto.Util.Option.
-
-Section language.
-  Context {base_type_code : Type}
-          {op : flat_type base_type_code -> flat_type base_type_code -> Type}
-          {Name : Type}
-          {interp_base_type : base_type_code -> Type}
-          {Context : Context Name interp_base_type}
-          {interp_op : forall s d, op s d -> interp_flat_type interp_base_type s -> interp_flat_type interp_base_type d}
-          {interped_op_side_conditions : forall s d, op s d -> interp_flat_type interp_base_type s -> pointed_Prop}.
-
-  Local Notation exprf := (@exprf base_type_code op Name).
-  Local Notation expr := (@expr base_type_code op Name).
-
-  Lemma snd_interpf_side_conditions_gen_eq {t} {ctx : Context} {e}
-    : interpf (t:=t) (ctx:=ctx) (interp_op:=interp_op) e
-      = option_map (@snd _ _) (interpf_side_conditions_gen interp_op interped_op_side_conditions ctx e).
-  Proof.
-    revert ctx; induction e; intros;
-      repeat first [ reflexivity
-                   | progress subst
-                   | progress inversion_option
-                   | progress unfold option_map, LetIn.Let_In in *
-                   | break_innermost_match_step
-                   | break_innermost_match_hyps_step
-                   | progress simpl in *
-                   | match goal with
-                     | [ H : forall ctx, interpf ?e = _, H' : context[interpf ?e] |- _ ]
-                       => rewrite H in H'
-                     | [ H : forall ctx, interpf ?e = _ |- context[interpf ?e] ]
-                       => rewrite H
-                     end ].
-  Qed.
-  Lemma snd_interpf_side_conditions_gen_Some {t} {ctx : Context} {e v}
-    : interpf (t:=t) (ctx:=ctx) (interp_op:=interp_op) e = Some v
-      <-> option_map (@snd _ _) (interpf_side_conditions_gen interp_op interped_op_side_conditions ctx e) = Some v.
-  Proof. rewrite snd_interpf_side_conditions_gen_eq; reflexivity. Qed.
-End language.