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