blob: 8ea8aa5c91f1f70de1486bb903a1b8ffb9857059 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
|
Require Import Crypto.Specific.Framework.SynthesisFramework.
Require Import Crypto.Specific.X2448.Karatsuba.C64.CurveParameters.
Module Import T := MakeSynthesisTactics Curve.
Module P <: SynthesisPrePackage.
Definition Synthesis_package' : Synthesis_package'_Type.
Proof. make_synthesis_package (). Defined.
Definition Synthesis_package
:= Eval cbv [Synthesis_package' projT2] in projT2 Synthesis_package'.
End P.
Module Export S := PackageSynthesis Curve P.
|
