blob: 863f765c2ded4f85ed74dadeb6dc543a4b9f22cb (
plain)
1
2
3
4
5
6
7
8
9
|
Require Import Crypto.Specific.Framework.SynthesisFramework.
Require Import Crypto.Specific.solinas32_2e174m3_7limbs.CurveParameters.
Module P <: PrePackage.
Definition package : Tag.Context.
Proof. make_Synthesis_package curve extra_prove_mul_eq extra_prove_square_eq. Defined.
End P.
Module Export S := PackageSynthesis P.
|
