1 files changed, 0 insertions, 61 deletions
diff --git a/src/Specific/Framework/ArithmeticSynthesis/KaratsubaPackage.v b/src/Specific/Framework/ArithmeticSynthesis/KaratsubaPackage.v
deleted file mode 100644
index 197c9431b..000000000
--- a/src/Specific/Framework/ArithmeticSynthesis/KaratsubaPackage.v
+++ /dev/null
@@ -1,61 +0,0 @@
-(* This file is autogenerated from Karatsuba.v by remake_packages.py *)
-Require Import Crypto.Specific.Framework.CurveParametersPackage.
-Require Import Crypto.Specific.Framework.ArithmeticSynthesis.BasePackage.
-Require Import Crypto.Specific.Framework.ArithmeticSynthesis.DefaultsPackage.
-Require Export Crypto.Specific.Framework.ArithmeticSynthesis.Karatsuba.
-Require Import Crypto.Specific.Framework.Packages.
-Require Import Crypto.Util.TagList.
-
-Module TAG.
-  Inductive tags := half_sz_nonzero.
-End TAG.
-
-Ltac add_half_sz_nonzero pkg :=
-  if_goldilocks
-    pkg
-    ltac:(fun _ => let half_sz := Tag.get pkg TAG.half_sz in
-                   let half_sz_nonzero := fresh "half_sz_nonzero" in
-                   let half_sz_nonzero := pose_half_sz_nonzero half_sz half_sz_nonzero in
-                   Tag.update pkg TAG.half_sz_nonzero half_sz_nonzero)
-    ltac:(fun _ => pkg)
-    ().
-Ltac add_mul_sig pkg :=
-  if_goldilocks
-    pkg
-    ltac:(fun _ => let wt := Tag.get pkg TAG.wt in
-                   let m := Tag.get pkg TAG.m in
-                   let base := Tag.get pkg TAG.base in
-                   let sz := Tag.get pkg TAG.sz in
-                   let s := Tag.get pkg TAG.s in
-                   let c := Tag.get pkg TAG.c in
-                   let half_sz := Tag.get pkg TAG.half_sz in
-                   let mul_sig := fresh "mul_sig" in
-                   let mul_sig := pose_mul_sig wt m base sz s c half_sz mul_sig in
-                   Tag.update pkg TAG.mul_sig mul_sig)
-    ltac:(fun _ => pkg)
-    ().
-Ltac add_square_sig pkg :=
-  if_goldilocks
-    pkg
-    ltac:(fun _ => let sz := Tag.get pkg TAG.sz in
-                   let m := Tag.get pkg TAG.m in
-                   let wt := Tag.get pkg TAG.wt in
-                   let mul_sig := Tag.get pkg TAG.mul_sig in
-                   let square_sig := fresh "square_sig" in
-                   let square_sig := pose_square_sig sz m wt mul_sig square_sig in
-                   Tag.update pkg TAG.square_sig square_sig)
-    ltac:(fun _ => pkg)
-    ().
-Ltac add_Karatsuba_package pkg :=
-  let pkg := add_half_sz_nonzero pkg in
-  let pkg := add_mul_sig pkg in
-  let pkg := add_square_sig pkg in
-  Tag.strip_subst_local pkg.
-
-
-Module MakeKaratsubaPackage (PKG : PrePackage).
-  Module Import MakeKaratsubaPackageInternal := MakePackageBase PKG.
-
-  Ltac get_half_sz_nonzero _ := get TAG.half_sz_nonzero.
-  Notation half_sz_nonzero := (ltac:(let v := get_half_sz_nonzero () in exact v)) (only parsing).
-End MakeKaratsubaPackage.