aboutsummaryrefslogtreecommitdiff
path: root/src/Spec/CompleteEdwardsCurve.v
diff options
context:
space:
mode:
authorGravatar Jason Gross <jagro@google.com>2016-06-22 13:54:20 -0700
committerGravatar Jason Gross <jagro@google.com>2016-06-22 13:54:20 -0700
commita4c50ceb1c773c8b1f36a5409c2112cf80725f7e (patch)
tree50f362f2dfa93bc4cb72034a0a1c42750a8af65d /src/Spec/CompleteEdwardsCurve.v
parent585e947def4cce90241a361032344e323e15d48b (diff)
Fix broken notations (hopefully)
Diffstat (limited to 'src/Spec/CompleteEdwardsCurve.v')
-rw-r--r--src/Spec/CompleteEdwardsCurve.v4
1 files changed, 2 insertions, 2 deletions
diff --git a/src/Spec/CompleteEdwardsCurve.v b/src/Spec/CompleteEdwardsCurve.v
index 06c3f8fdb..f6db1c14f 100644
--- a/src/Spec/CompleteEdwardsCurve.v
+++ b/src/Spec/CompleteEdwardsCurve.v
@@ -13,7 +13,7 @@ Module E.
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) (at level 30).
+ Local Notation "x ^ 2" := (x*x) (at level 30).
Context {a d: F}.
Class twisted_edwards_params :=
@@ -50,4 +50,4 @@ End E.
Delimit Scope E_scope with E.
Infix "+" := E.add : E_scope.
-Infix "*" := E.mul : E_scope. \ No newline at end of file
+Infix "*" := E.mul : E_scope.