blob: 28806adeef8c512f454f54d6be83b563d1eadb5d (
plain)
1
2
3
4
5
6
7
8
9
|
Require Import Crypto.Specific.Framework.SynthesisFramework.
Require Import Crypto.Specific.solinas32_2e222m117_9limbs.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.
|