1 files changed, 38 insertions, 0 deletions
diff --git a/src/Specific/Framework/ArithmeticSynthesis/LadderstepPackage.v b/src/Specific/Framework/ArithmeticSynthesis/LadderstepPackage.v
new file mode 100644
index 000000000..dd7b6c541
--- /dev/null
+++ b/src/Specific/Framework/ArithmeticSynthesis/LadderstepPackage.v
@@ -0,0 +1,38 @@
+(* 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 := Mxzladderstep_sig.
+End TAG.
+
+Ltac add_Mxzladderstep_sig pkg :=
+  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 add_Ladderstep_package pkg :=
+  let pkg := add_Mxzladderstep_sig pkg in
+  Tag.strip_local pkg.
+
+
+Module MakeLadderstepPackage (PKG : PrePackage).
+  Module Import MakeLadderstepPackageInternal := MakePackageBase PKG.
+
+  Ltac get_Mxzladderstep_sig _ := get TAG.Mxzladderstep_sig.
+  Notation Mxzladderstep_sig := (ltac:(let v := get_Mxzladderstep_sig () in exact v)) (only parsing).
+End MakeLadderstepPackage.