blob: c5a9e0fd38d06d4345fc27441196d5f6c6c19bc2 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
|
Require Import Crypto.Specific.ReificationTypes.
Require Import Crypto.Specific.X25519.C32.ArithmeticSynthesisTest.
Module RP <: ReificationTypesPrePackage.
Definition ReificationTypes_package' : { T : _ & T }.
Proof. make_ReificationTypes_package wt sz bounds m wt_nonneg P.upper_bound_of_exponent. Defined.
Definition ReificationTypes_package
:= Eval cbv [ReificationTypes_package' projT2] in projT2 ReificationTypes_package'.
End RP.
Module Export ReificationTypes := MakeReificationTypes RP.
|
