diff options
Diffstat (limited to 'src/CompleteEdwardsCurve/Pre.v')
| -rw-r--r-- | src/CompleteEdwardsCurve/Pre.v | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/src/CompleteEdwardsCurve/Pre.v b/src/CompleteEdwardsCurve/Pre.v index 5314ee37c..7e9f14321 100644 --- a/src/CompleteEdwardsCurve/Pre.v +++ b/src/CompleteEdwardsCurve/Pre.v @@ -1,5 +1,6 @@ Require Import Coq.Classes.Morphisms. Require Coq.Setoids.Setoid. Require Import Crypto.Algebra Crypto.Tactics.Nsatz. +Require Import Crypto.Util.Notations. Generalizable All Variables. Section Pre. @@ -9,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) (at level 30). + Local Notation "x ^2" := (x*x). Add Field EdwardsCurveField : (Field.field_theory_for_stdlib_tactic (T:=F)). @@ -97,4 +98,4 @@ Section RespectsFieldHomomorphism. apply conj; (rewrite_strat topdown hints field_homomorphism); reflexivity. Qed. -End RespectsFieldHomomorphism.
\ No newline at end of file +End RespectsFieldHomomorphism. |