blob: 500671c90a40e240be476b14cb6b20d51a40b3f7 (
plain)
1
2
3
4
5
6
7
8
9
10
11
|
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.
End P.
Module Export S := PackageSynthesis Curve P.
|
