diff options
| -rw-r--r-- | src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v | 4 | ||||
| -rw-r--r-- | src/CompleteEdwardsCurve/ExtendedCoordinates.v | 2 | ||||
| -rw-r--r-- | src/CompleteEdwardsCurve/Pre.v | 2 | ||||
| -rw-r--r-- | src/Spec/CompleteEdwardsCurve.v | 4 | ||||
| -rw-r--r-- | src/Util/Notations.v | 4 |
5 files changed, 8 insertions, 8 deletions
diff --git a/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v b/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v index c217303aa..476592b36 100644 --- a/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v +++ b/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v @@ -19,7 +19,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). + Local Notation "x ^ 2" := (x*x). Local Notation point := (@point F Feq Fone Fadd Fmul a d). Local Notation onCurve := (@onCurve F Feq Fone Fadd Fmul a d). @@ -159,7 +159,7 @@ Module E. Admitted. Section PointCompression. - Local Notation "x ^2" := (x*x). + Local Notation "x ^ 2" := (x*x). Definition solve_for_x2 (y : F) := ((y^2 - 1) / (d * (y^2) - a)). Lemma a_d_y2_nonzero : forall y, d * y^2 - a <> 0. 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). 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)). 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. diff --git a/src/Util/Notations.v b/src/Util/Notations.v index ffa42e054..bbeb50092 100644 --- a/src/Util/Notations.v +++ b/src/Util/Notations.v @@ -11,8 +11,8 @@ Reserved Infix "?=" (at level 70, no associativity). Reserved Infix "?<" (at level 70, no associativity). Reserved Infix ".+" (at level 50). Reserved Infix ".*" (at level 50). -Reserved Notation "x ^2" (at level 30, format "x ^2"). -Reserved Notation "x ^3" (at level 30, format "x ^3"). +Reserved Notation "x ^ 2" (at level 30, format "x ^ 2"). +Reserved Notation "x ^ 3" (at level 30, format "x ^ 3"). Reserved Infix "mod" (at level 40, no associativity). Reserved Notation "'canonical' 'encoding' 'of' T 'as' B" (at level 50). Reserved Infix "<<" (at level 50). |