1 files changed, 0 insertions, 89 deletions
diff --git a/src/Compilers/Named/InterpretToPHOASInterp.v b/src/Compilers/Named/InterpretToPHOASInterp.v
deleted file mode 100644
index 7fe50c994..000000000
--- a/src/Compilers/Named/InterpretToPHOASInterp.v
+++ /dev/null
@@ -1,89 +0,0 @@
-Require Import Crypto.Compilers.Named.Context.
-Require Import Crypto.Compilers.Named.Syntax.
-Require Import Crypto.Compilers.Named.Wf.
-Require Import Crypto.Compilers.Named.ContextDefinitions.
-Require Import Crypto.Compilers.Named.ContextProperties.
-Require Import Crypto.Compilers.Named.InterpretToPHOAS.
-Require Import Crypto.Compilers.Syntax.
-Require Import Crypto.Compilers.Wf.
-Require Import Crypto.Util.PointedProp.
-Require Import Crypto.Util.Decidable.
-Require Import Crypto.Util.Option.
-Require Import Crypto.Util.Tactics.BreakMatch.
-Require Import Crypto.Util.Tactics.DestructHead.
-
-Section language.
-  Context {base_type_code : Type}
-          {op : flat_type base_type_code -> flat_type base_type_code -> Type}
-          {Name : Type}
-          {base_type_code_dec : DecidableRel (@eq base_type_code)}
-          {Name_dec : DecidableRel (@eq Name)}
-          {interp_base_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}.
-  Section with_context.
-    Context {Context : Context Name interp_base_type}
-            {ContextOk : ContextOk Context}
-            (failb : forall t, @Syntax.exprf base_type_code op interp_base_type (Tbase t)).
-
-    Lemma interpf_interpf_to_phoas
-          (ctx : Context)
-          {t} (e : @Named.exprf base_type_code op Name t)
-          (Hwf : prop_of_option (Named.wff ctx e))
-      : Named.interpf (interp_op:=interp_op) (ctx:=ctx) e
-        = Some (Syntax.interpf interp_op (interpf_to_phoas failb ctx e)).
-    Proof using Type.
-      revert dependent ctx; induction e;
-        repeat first [ progress intros
-                     | progress subst
-                     | progress inversion_option
-                     | progress destruct_head' and
-                     | progress break_innermost_match_step
-                     | progress unfold option_map, LetIn.Let_In in *
-                     | apply (f_equal (@Some _))
-                     | apply (f_equal (@interp_op _ _ _))
-                     | progress simpl in *
-                     | progress autorewrite with push_prop_of_option in *
-                     | solve [ eauto | congruence | tauto ]
-                     | match goal with
-                       | [ H : forall ctx Hwf', Named.interpf ?e = Some _, Hwf : prop_of_option (Named.wff _ ?e) |- _ ]
-                         => specialize (H _ Hwf)
-                       | [ H : forall ctx Hwf, Named.interpf ?e = Some _ |- Named.interpf ?e = Some _ ]
-                         => rewrite H by auto
-                       end ].
-    Qed.
-
-    Lemma interp_interp_to_phoas
-          (ctx : Context)
-          {t} (e : @Named.expr base_type_code op Name t)
-          (Hwf : Named.wf ctx e)
-          v
-      : Named.interp (interp_op:=interp_op) (ctx:=ctx) e v
-        = Some (Syntax.interp interp_op (interp_to_phoas failb ctx e) v).
-    Proof using Type.
-      unfold interp, interp_to_phoas, Named.interp; apply interpf_interpf_to_phoas; auto.
-    Qed.
-  End with_context.
-
-  Section all.
-    Context {Context : forall var, @Context base_type_code Name var}
-            {ContextOk : forall var, ContextOk (Context var)}
-            (failb : forall var t, @Syntax.exprf base_type_code op var (Tbase t)).
-
-    Lemma Interp_InterpToPHOAS_gen
-          {ctx : forall var, Context var}
-          {t} (e : @Named.expr base_type_code op Name t)
-          (Hwf : forall var, Named.wf (ctx var) e)
-          v
-      : Named.interp (interp_op:=interp_op) (ctx:=ctx _) e v
-        = Some (Interp interp_op (InterpToPHOAS_gen failb ctx e) v).
-    Proof using Type. apply interp_interp_to_phoas; auto. Qed.
-
-    Lemma Interp_InterpToPHOAS
-          {t} (e : @Named.expr base_type_code op Name t)
-          (Hwf : Named.Wf Context e)
-          v
-      : Named.Interp (Context:=Context _) (interp_op:=interp_op) e v
-        = Some (Interp interp_op (InterpToPHOAS (Context:=Context) failb e) v).
-    Proof using Type. apply interp_interp_to_phoas; auto. Qed.
-  End all.
-End language.