2 files changed, 24 insertions, 26 deletions
diff --git a/src/Specific/X2448/Karatsuba/C64/CurveParameters.v b/src/Specific/X2448/Karatsuba/C64/CurveParameters.v
index cc8393d9b..7302294b8 100644
--- a/src/Specific/X2448/Karatsuba/C64/CurveParameters.v
+++ b/src/Specific/X2448/Karatsuba/C64/CurveParameters.v
@@ -1,4 +1,4 @@
-Require Import Crypto.Specific.Framework.CurveParameters.
+Require Import Crypto.Specific.Framework.RawCurveParameters.
 Require Import Crypto.Util.LetIn.
 
 (***
@@ -6,29 +6,29 @@ Modulus : 2^448-2^224-1
 Base: 56
 ***)
 
-Module Curve <: CurveParameters.
-  Definition sz : nat := 8%nat.
-  Definition bitwidth : Z := 64.
-  Definition s : Z := 2^448.
-  Definition c : list limb := [(1, 1); (2^224, 1)].
-  Definition carry_chains : option (list (list nat)) := Eval vm_compute in Some [[3; 7]; [0; 4; 1; 5; 2; 6; 3; 7]; [4; 0]]%nat.
+Definition curve : CurveParameters :=
+  {|
+    sz := 8%nat;
+    bitwidth := 64;
+    s := 2^448;
+    c := [(1, 1); (2^224, 1)];
+    carry_chains := Some [[3; 7]; [0; 4; 1; 5; 2; 6; 3; 7]; [4; 0]]%nat;
 
-  Definition a24 : option Z := None.
-  Definition coef_div_modulus : option nat := Some 2%nat. (* add 2*modulus before subtracting *)
+    a24 := None;
+    coef_div_modulus := Some 2%nat;
 
-  Definition goldilocks : bool := true.
-  Definition montgomery : bool := false.
+    goldilocks := Some true;
+    montgomery := false;
 
-  Definition mul_code : option (Z^sz -> Z^sz -> Z^sz)
-    := None.
+    mul_code := None;
 
-  Definition square_code : option (Z^sz -> Z^sz)
-    := None.
+    square_code := None;
 
-  Definition upper_bound_of_exponent : option (Z -> Z) := None.
-  Definition allowable_bit_widths : option (list nat) := None.
-  Definition freeze_extra_allowable_bit_widths : option (list nat) := None.
-  Definition modinv_fuel : option nat := None.
-  Ltac extra_prove_mul_eq := idtac.
-  Ltac extra_prove_square_eq := idtac.
-End Curve.
+    upper_bound_of_exponent := None;
+    allowable_bit_widths := None;
+    freeze_extra_allowable_bit_widths := None;
+    modinv_fuel := None
+  |}.
+
+Ltac extra_prove_mul_eq _ := idtac.
+Ltac extra_prove_square_eq _ := idtac.
diff --git a/src/Specific/X2448/Karatsuba/C64/Synthesis.v b/src/Specific/X2448/Karatsuba/C64/Synthesis.v
index 500671c90..4016ee71c 100644
--- a/src/Specific/X2448/Karatsuba/C64/Synthesis.v
+++ b/src/Specific/X2448/Karatsuba/C64/Synthesis.v
@@ -1,11 +1,9 @@
 Require Import Crypto.Specific.Framework.SynthesisFramework.
 Require Import Crypto.Specific.X2448.Karatsuba.C64.CurveParameters.
 
-Module Import T := MakeSynthesisTactics Curve.
-
 Module P <: PrePackage.
   Definition package : Tag.Context.
-  Proof. make_Synthesis_package (). Defined.
+  Proof. make_Synthesis_package curve extra_prove_mul_eq extra_prove_square_eq. Defined.
 End P.
 
-Module Export S := PackageSynthesis Curve P.
+Module Export S := PackageSynthesis P.