aboutsummaryrefslogtreecommitdiff
path: root/src/Spec
diff options
context:
space:
mode:
Diffstat (limited to 'src/Spec')
-rw-r--r--src/Spec/Ed25519.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/Spec/Ed25519.v b/src/Spec/Ed25519.v
index 150e3f388..bdafa10fe 100644
--- a/src/Spec/Ed25519.v
+++ b/src/Spec/Ed25519.v
@@ -11,7 +11,7 @@ Section Ed25519.
Definition q : BinNums.Z := 2^255 - 19.
Definition Fq : Type := F q.
- Definition l : BinNums.Z := 252 + 27742317777372353535851937790883648493.
+ Definition l : BinNums.Z := 2^252 + 27742317777372353535851937790883648493.
Definition Fl : Type := F l.
Local Open Scope F_scope.