1 files changed, 0 insertions, 81 deletions
diff --git a/src/Compilers/ZExtended/Syntax/Util.v b/src/Compilers/ZExtended/Syntax/Util.v
deleted file mode 100644
index 7c3ed70e6..000000000
--- a/src/Compilers/ZExtended/Syntax/Util.v
+++ /dev/null
@@ -1,81 +0,0 @@
-Require Import Crypto.Compilers.SmartMap.
-Require Import Crypto.Compilers.ExprInversion.
-Require Import Crypto.Compilers.Syntax.
-Require Import Crypto.Compilers.Z.Syntax.
-Require Import Crypto.Compilers.ZExtended.Syntax.
-
-Definition unextend_base_type (t : ZExtended.Syntax.base_type) : Z.Syntax.base_type
-  := match t with
-     | TZ => Z.Syntax.TZ
-     | TBool => Z.Syntax.TZ
-     end.
-
-Definition invert_Const s d (opc : op s d) : option (interp_flat_type interp_base_type d)
-  := match opc with
-     | ConstZ v => Some v
-     | ConstBool v => Some v
-     | AddWithGetCarry
-     | SubWithGetBorrow
-     | MulSplitAtBitwidth
-     | AddWithGetCarryZ _
-     | SubWithGetBorrowZ _
-     | MulSplitAtBitwidthZ _
-     | IdWithAlt _
-     | Zselect
-     | Zmul
-     | Zadd
-     | Zsub
-     | Zopp
-     | Zshiftr
-     | Zshiftl
-     | Zland
-     | Zlor
-     | Zmodulo
-     | Zdiv
-     | Zlog2
-     | Zpow
-     | Zones
-     | Zeqb
-     | BoolCase _
-       => None
-     end.
-
-Definition unextend_op {s d} (opc : ZExtended.Syntax.op s d)
-  : option (Z.Syntax.op (lift_flat_type unextend_base_type s)
-                        (lift_flat_type unextend_base_type d))
-  := match opc in ZExtended.Syntax.op s d
-           return option (Z.Syntax.op (lift_flat_type unextend_base_type s)
-                                      (lift_flat_type unextend_base_type d))
-     with
-     | AddWithGetCarry => None
-     | AddWithGetCarryZ bitwidth
-       => Some (Z.Syntax.AddWithGetCarry bitwidth _ _ _ _ _)
-     | SubWithGetBorrow => None
-     | SubWithGetBorrowZ bitwidth
-       => Some (Z.Syntax.SubWithGetBorrow bitwidth _ _ _ _ _)
-     | MulSplitAtBitwidth => None
-     | MulSplitAtBitwidthZ bitwidth
-       => Some (Z.Syntax.MulSplit bitwidth _ _ _ _)
-     | IdWithAlt (Tbase _)
-       => Some (Z.Syntax.IdWithAlt _ _ _)
-     | IdWithAlt _
-       => None
-     | Zselect => Some (Z.Syntax.Zselect _ _ _ _)
-     | Zmul => Some (Z.Syntax.Mul _ _ _)
-     | Zadd => Some (Z.Syntax.Add _ _ _)
-     | Zsub => Some (Z.Syntax.Sub _ _ _)
-     | Zopp => Some (Z.Syntax.Opp _ _)
-     | Zshiftr => Some (Z.Syntax.Shr _ _ _)
-     | Zshiftl => Some (Z.Syntax.Shl _ _ _)
-     | Zland => Some (Z.Syntax.Land _ _ _)
-     | Zlor => Some (Z.Syntax.Lor _ _ _)
-     | Zmodulo => None
-     | Zdiv => None
-     | Zlog2 => None
-     | Zpow => None
-     | Zones => None
-     | Zeqb => None
-     | ConstZ v => Some (OpConst v)
-     | ConstBool v => None
-     | BoolCase T => None
-     end.