1 files changed, 0 insertions, 54 deletions
diff --git a/src/Compilers/Named/InterpSideConditions.v b/src/Compilers/Named/InterpSideConditions.v
deleted file mode 100644
index bd90eac23..000000000
--- a/src/Compilers/Named/InterpSideConditions.v
+++ /dev/null
@@ -1,54 +0,0 @@
-Require Import Crypto.Compilers.Syntax.
-Require Import Crypto.Compilers.Named.Syntax.
-Require Import Crypto.Compilers.Named.Context.
-Require Import Crypto.Util.PointedProp.
-Require Import Crypto.Util.Notations.
-
-Module Export Named.
-  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).
-
-    Fixpoint interpf_side_conditions_gen {t} (ctx : Context) (e : exprf t)
-      : option (pointed_Prop * interp_flat_type interp_base_type t)
-      := match e with
-         | TT => Some (trivial, tt)
-         | Var t' x => option_map (fun v => (trivial, v)) (lookupb t' ctx x)
-         | Op t1 tR opc args
-           => match @interpf_side_conditions_gen _ ctx args with
-              | Some (args_cond, argsv)
-                => Some (args_cond /\ interped_op_side_conditions _ _ opc argsv, interp_op _ _ opc argsv)
-              | None => None
-              end
-         | LetIn _ n ex _ eC
-           => match @interpf_side_conditions_gen _ ctx ex with
-              | Some (x_cond, x)
-                => match @interpf_side_conditions_gen _ (extend ctx n x) eC with
-                   | Some (c_cond, cv)
-                     => Some (x_cond /\ c_cond, cv)
-                   | None => None
-                   end
-              | None => None
-              end
-         | Pair _ ex _ ey
-           => match @interpf_side_conditions_gen _ ctx ex, @interpf_side_conditions_gen _ ctx ey with
-              | Some (x_cond, xv), Some (y_cond, yv) => Some (x_cond /\ y_cond, (xv, yv))
-              | None, _ | _, None => None
-              end
-         end%pointed_prop.
-    Definition interpf_side_conditions {t} ctx e : option pointed_Prop
-      := option_map (@fst _ _) (@interpf_side_conditions_gen t ctx e).
-    Definition interp_side_conditions {t} ctx (e : expr t) : interp_flat_type interp_base_type (domain t) -> option pointed_Prop
-      := fun x => interpf_side_conditions (extend ctx (Abs_name e) x) (invert_Abs e).
-    Definition InterpSideConditions {t} (e : expr t) : interp_flat_type interp_base_type (domain t) -> option pointed_Prop
-      := interp_side_conditions empty e.
-  End language.
-End Named.