aboutsummaryrefslogtreecommitdiff
path: root/src/Curves/Curve25519.v
diff options
context:
space:
mode:
Diffstat (limited to 'src/Curves/Curve25519.v')
-rw-r--r--src/Curves/Curve25519.v1
1 files changed, 1 insertions, 0 deletions
diff --git a/src/Curves/Curve25519.v b/src/Curves/Curve25519.v
index ad04c1ec6..248e0af6e 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 := GaloisField Modulus25519.
+
Local Open Scope GF_scope.
Definition a : GF := -1.