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