diff options
Diffstat (limited to 'src/Curves/Curve25519.v')
-rw-r--r-- | src/Curves/Curve25519.v | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/src/Curves/Curve25519.v b/src/Curves/Curve25519.v index edcf6a24c..8bb2148db 100644 --- a/src/Curves/Curve25519.v +++ b/src/Curves/Curve25519.v @@ -10,6 +10,7 @@ End Modulus25519. Module Curve25519Params <: TwistedEdwardsParams Modulus25519 <: Minus1Params Modulus25519. Module Import GFDefs := GaloisDefs Modulus25519. + Local Open Scope GF_scope. Coercion inject : Z >-> GF. Definition a : GF := -1. |