aboutsummaryrefslogtreecommitdiff
path: root/src/CompleteEdwardsCurve/Pre.v
diff options
context:
space:
mode:
Diffstat (limited to 'src/CompleteEdwardsCurve/Pre.v')
-rw-r--r--src/CompleteEdwardsCurve/Pre.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/CompleteEdwardsCurve/Pre.v b/src/CompleteEdwardsCurve/Pre.v
index 7e9f14321..be294fb3e 100644
--- a/src/CompleteEdwardsCurve/Pre.v
+++ b/src/CompleteEdwardsCurve/Pre.v
@@ -10,7 +10,7 @@ Section Pre.
Local Notation "0" := zero. Local Notation "1" := one.
Local Infix "+" := add. Local Infix "*" := mul.
Local Infix "-" := sub. Local Infix "/" := div.
- Local Notation "x ^2" := (x*x).
+ Local Notation "x ^ 2" := (x*x).
Add Field EdwardsCurveField : (Field.field_theory_for_stdlib_tactic (T:=F)).