diff options
| author |  Robert Sloan <varomodt@dhcp-18-189-26-21.dyn.MIT.EDU> | 2015-09-17 10:43:22 -0400 |
|---|---|---|
| committer | Robert Sloan <varomodt@dhcp-18-189-26-21.dyn.MIT.EDU> | 2015-09-17 10:43:22 -0400 |
| commit | 810f1d9adf16235dd69f90cca512275585d0ef32 (patch) | |
| tree | 0541b31f04a972913c9427aae013c445dd883599 /src/Curves | |
| parent | 0d063eafadf1237db4b99debf896f61bca4aeef0 (diff) | |
fix module structure + add assembly placeholder
Diffstat (limited to 'src/Curves')
| -rw-r--r-- | src/Curves/Curve25519.v | 6 |
1 files changed, 2 insertions, 4 deletions
diff --git a/src/Curves/Curve25519.v b/src/Curves/Curve25519.v index df0b2ce06..8c34ea098 100644 --- a/src/Curves/Curve25519.v +++ b/src/Curves/Curve25519.v @@ -11,12 +11,10 @@ Module Modulus25519 <: Modulus. Definition modulus := prime25519. End Modulus25519. -Declare Module GaloisField25519 : GaloisField Modulus25519. - -Declare Module GaloisTheory25519 : GaloisFieldTheory Modulus25519 GaloisField25519. +Module GaloisTheory25519 := GaloisFieldTheory Modulus25519. Module Curve25519. - Import Modulus25519 GaloisField25519 GaloisTheory25519. + Import Modulus25519 GaloisTheory25519.Field GaloisTheory25519. (* Prove some theorems! *) End Curve25519. |