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