1 files changed, 0 insertions, 56 deletions
diff --git a/src/Compilers/Named/NameUtil.v b/src/Compilers/Named/NameUtil.v
deleted file mode 100644
index 8b099ffdf..000000000
--- a/src/Compilers/Named/NameUtil.v
+++ /dev/null
@@ -1,56 +0,0 @@
-Require Import Coq.Lists.List.
-Require Import Crypto.Compilers.Syntax.
-
-Local Open Scope core_scope.
-Local Notation eta x := (fst x, snd x).
-
-Section language.
-  Context {base_type_code : Type}
-          {Name : Type}.
-
-  Section monad.
-    Context (MName : Type) (force : MName -> option Name).
-    Fixpoint split_mnames
-             (t : flat_type base_type_code) (ls : list MName)
-      : option (interp_flat_type (fun _ => Name) t) * list MName
-      := match t return option (@interp_flat_type base_type_code (fun _ => Name) t) * _ with
-         | Tbase _
-           => match ls with
-              | cons n ls'
-                => match force n with
-                   | Some n => (Some n, ls')
-                   | None => (None, ls')
-                   end
-              | nil => (None, nil)
-              end
-         | Unit => (Some tt, ls)
-         | Prod A B
-           => let '(a, ls) := eta (@split_mnames A ls) in
-              let '(b, ls) := eta (@split_mnames B ls) in
-              (match a, b with
-               | Some a', Some b' => Some (a', b')
-               | _, _ => None
-               end,
-               ls)
-         end.
-    Definition mname_list_unique (ls : list MName) : Prop
-      := forall k n,
-        List.In (Some n) (firstn k (List.map force ls))
-        -> List.In (Some n) (skipn k (List.map force ls))
-        -> False.
-  End monad.
-  Definition split_onames := @split_mnames (option Name) (fun x => x).
-  Definition split_names := @split_mnames Name (@Some _).
-
-  Definition oname_list_unique (ls : list (option Name)) : Prop
-    := mname_list_unique (option Name) (fun x => x) ls.
-  Definition name_list_unique (ls : list Name) : Prop
-    := oname_list_unique (List.map (@Some Name) ls).
-End language.
-
-Global Arguments split_mnames {_ _ MName} force _ _, {_ _} MName force _ _.
-Global Arguments split_onames {_ _} _ _.
-Global Arguments split_names {_ _} _ _.
-Global Arguments mname_list_unique {_ MName} force ls, {_} MName force ls.
-Global Arguments oname_list_unique {_} ls.
-Global Arguments name_list_unique {_} ls.