aboutsummaryrefslogtreecommitdiff
path: root/src/CompleteEdwardsCurve/ExtendedCoordinates.v
diff options
context:
space:
mode:
Diffstat (limited to 'src/CompleteEdwardsCurve/ExtendedCoordinates.v')
-rw-r--r--src/CompleteEdwardsCurve/ExtendedCoordinates.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/CompleteEdwardsCurve/ExtendedCoordinates.v b/src/CompleteEdwardsCurve/ExtendedCoordinates.v
index e2ffa0313..deeb795b1 100644
--- a/src/CompleteEdwardsCurve/ExtendedCoordinates.v
+++ b/src/CompleteEdwardsCurve/ExtendedCoordinates.v
@@ -19,7 +19,7 @@ Module Extended.
Local Notation "0" := Fzero. Local Notation "1" := Fone.
Local Infix "+" := Fadd. Local Infix "*" := Fmul.
Local Infix "-" := Fsub. Local Infix "/" := Fdiv.
- Local Notation "x ^2" := (x*x).
+ Local Notation "x ^ 2" := (x*x).
Local Notation Epoint := (@E.point F Feq Fone Fadd Fmul a d).
Local Notation onCurve := (@Pre.onCurve F Feq Fone Fadd Fmul a d).