1 files changed, 0 insertions, 27 deletions
diff --git a/src/Compilers/Named/IdContext.v b/src/Compilers/Named/IdContext.v
deleted file mode 100644
index d82740cb4..000000000
--- a/src/Compilers/Named/IdContext.v
+++ /dev/null
@@ -1,27 +0,0 @@
-Require Import Coq.Lists.List.
-Require Import Crypto.Compilers.Syntax.
-Require Import Crypto.Compilers.Named.Context.
-Require Import Crypto.Compilers.Named.Syntax.
-
-Section language.
-  Context {base_type_code Name}
-          {op : flat_type base_type_code -> flat_type base_type_code -> Type}
-          (Context : @Context base_type_code Name (fun _ => Name)).
-
-  Fixpoint collect_binders {t} (e : Named.exprf base_type_code op Name t)
-    : list { t : flat_type base_type_code & interp_flat_type (fun _ => Name) t }
-    := match e with
-       | TT => nil
-       | Var t n => (existT _ (Tbase t) n) :: nil
-       | Op t1 tR opc args => @collect_binders _ args
-       | LetIn tx n ex tC eC
-         => (existT _ tx n) :: @collect_binders tx ex ++ @collect_binders tC eC
-       | Pair tx ex ty ey
-         => @collect_binders tx ex ++ @collect_binders ty ey
-       end%list.
-  Definition idcontext {t} (e : Named.exprf base_type_code op Name t) : Context
-    := List.fold_right
-         (fun v ctx => extend ctx (projT2 v) (projT2 v))
-         empty
-         (collect_binders e).
-End language.