1 files changed, 38 insertions, 0 deletions
diff --git a/src/Specific/Framework/CurveParametersPackage.v b/src/Specific/Framework/CurveParametersPackage.v
new file mode 100644
index 000000000..782ccdd22
--- /dev/null
+++ b/src/Specific/Framework/CurveParametersPackage.v
@@ -0,0 +1,38 @@
+(* This file is autogenerated from CurveParameters.v by remake_packages.py *)
+Require Export Crypto.Specific.Framework.CurveParameters.
+Require Import Crypto.Specific.Framework.Packages.
+Require Import Crypto.Util.TagList.
+
+Ltac if_goldilocks pkg tac_true tac_false arg :=
+  let goldilocks := Tag.get pkg TAG.goldilocks in
+  let goldilocks := (eval vm_compute in (goldilocks : bool)) in
+  lazymatch goldilocks with
+  | true => tac_true arg
+  | false => tac_false arg
+  end.
+
+
+Module MakeCurveParametersPackage (PKG : PrePackage).
+  Module Import MakeCurveParametersPackageInternal := MakePackageBase PKG.
+
+  Ltac get_sz _ := get TAG.sz.
+  Notation sz := (ltac:(let v := get_sz () in exact v)) (only parsing).
+  Ltac get_bitwidth _ := get TAG.bitwidth.
+  Notation bitwidth := (ltac:(let v := get_bitwidth () in exact v)) (only parsing).
+  Ltac get_s _ := get TAG.s.
+  Notation s := (ltac:(let v := get_s () in exact v)) (only parsing).
+  Ltac get_c _ := get TAG.c.
+  Notation c := (ltac:(let v := get_c () in exact v)) (only parsing).
+  Ltac get_carry_chains _ := get TAG.carry_chains.
+  Notation carry_chains := (ltac:(let v := get_carry_chains () in exact v)) (only parsing).
+  Ltac get_a24 _ := get TAG.a24.
+  Notation a24 := (ltac:(let v := get_a24 () in exact v)) (only parsing).
+  Ltac get_coef_div_modulus _ := get TAG.coef_div_modulus.
+  Notation coef_div_modulus := (ltac:(let v := get_coef_div_modulus () in exact v)) (only parsing).
+  Ltac get_goldilocks _ := get TAG.goldilocks.
+  Notation goldilocks := (ltac:(let v := get_goldilocks () in exact v)) (only parsing).
+  Ltac get_modinv_fuel _ := get TAG.modinv_fuel.
+  Notation modinv_fuel := (ltac:(let v := get_modinv_fuel () in exact v)) (only parsing).
+  Ltac get_upper_bound_of_exponent _ := get TAG.upper_bound_of_exponent.
+  Notation upper_bound_of_exponent := (ltac:(let v := get_upper_bound_of_exponent () in exact v)) (only parsing).
+End MakeCurveParametersPackage.