1 files changed, 0 insertions, 75 deletions
diff --git a/src/Specific/Framework/ArithmeticSynthesis/LadderstepPackage.v b/src/Specific/Framework/ArithmeticSynthesis/LadderstepPackage.v
deleted file mode 100644
index 4108c8352..000000000
--- a/src/Specific/Framework/ArithmeticSynthesis/LadderstepPackage.v
+++ /dev/null
@@ -1,75 +0,0 @@
-(* This file is autogenerated from Ladderstep.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.Ladderstep.
-Require Import Crypto.Specific.Framework.Packages.
-Require Import Crypto.Util.TagList.
-
-Module TAG.
-  Inductive tags := a24' | a24_sig | Mxzladderstep_sig.
-End TAG.
-
-Ltac add_a24' pkg :=
-  if_ladderstep
-    pkg
-    ltac:(fun _ => Tag.update_by_tac_if_not_exists
-                       pkg
-                       TAG.a24'
-                       ltac:(fun _ => let a24 := Tag.get pkg TAG.a24 in
-                                      let a24' := fresh "a24'" in
-                                      let a24' := pose_a24' a24 a24' in
-                                      constr:(a24')))
-    ltac:(fun _ => pkg)
-    ().
-Ltac add_a24_sig pkg :=
-  if_ladderstep
-    pkg
-    ltac:(fun _ => Tag.update_by_tac_if_not_exists
-                       pkg
-                       TAG.a24_sig
-                       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 a24' := Tag.get pkg TAG.a24' in
-                                      let a24_sig := fresh "a24_sig" in
-                                      let a24_sig := pose_a24_sig sz m wt a24' a24_sig in
-                                      constr:(a24_sig)))
-    ltac:(fun _ => pkg)
-    ().
-Ltac add_Mxzladderstep_sig pkg :=
-  if_ladderstep
-    pkg
-    ltac:(fun _ => Tag.update_by_tac_if_not_exists
-                       pkg
-                       TAG.Mxzladderstep_sig
-                       ltac:(fun _ => let sz := Tag.get pkg TAG.sz in
-                                      let wt := Tag.get pkg TAG.wt in
-                                      let m := Tag.get pkg TAG.m in
-                                      let add_sig := Tag.get pkg TAG.add_sig in
-                                      let sub_sig := Tag.get pkg TAG.sub_sig in
-                                      let mul_sig := Tag.get pkg TAG.mul_sig in
-                                      let square_sig := Tag.get pkg TAG.square_sig in
-                                      let carry_sig := Tag.get pkg TAG.carry_sig in
-                                      let Mxzladderstep_sig := fresh "Mxzladderstep_sig" in
-                                      let Mxzladderstep_sig := pose_Mxzladderstep_sig sz wt m add_sig sub_sig mul_sig square_sig carry_sig Mxzladderstep_sig in
-                                      constr:(Mxzladderstep_sig)))
-    ltac:(fun _ => pkg)
-    ().
-Ltac add_Ladderstep_package pkg :=
-  let pkg := add_a24' pkg in
-  let pkg := add_a24_sig pkg in
-  let pkg := add_Mxzladderstep_sig pkg in
-  Tag.strip_subst_local pkg.
-
-
-Module MakeLadderstepPackage (PKG : PrePackage).
-  Module Import MakeLadderstepPackageInternal := MakePackageBase PKG.
-
-  Ltac get_a24' _ := get TAG.a24'.
-  Notation a24' := (ltac:(let v := get_a24' () in exact v)) (only parsing).
-  Ltac get_a24_sig _ := get TAG.a24_sig.
-  Notation a24_sig := (ltac:(let v := get_a24_sig () in exact v)) (only parsing).
-  Ltac get_Mxzladderstep_sig _ := get TAG.Mxzladderstep_sig.
-  Notation Mxzladderstep_sig := (ltac:(let v := get_Mxzladderstep_sig () in exact v)) (only parsing).
-End MakeLadderstepPackage.