point_eq_dec

2 files changed, 5 insertions, 5 deletions

diff --git a/src/Spec/CompleteEdwardsCurve.v b/src/Spec/CompleteEdwardsCurve.v
index b7d2c0d8e..8dbfdf7b9 100644
--- a/src/Spec/CompleteEdwardsCurve.v
+++ b/src/Spec/CompleteEdwardsCurve.v
@@ -46,11 +46,8 @@ Section TwistedEdwardsCurves.
     | O => zero
     | S n' => unifiedAdd P (scalarMult n' P)
     end.
-
-  Axiom point_eq_dec : forall P Q : point, {P = Q} + {P <> Q}.
 End TwistedEdwardsCurves.
 
 Delimit Scope E_scope with E.
 Infix "+" := unifiedAdd : E_scope.
-Infix "*" := scalarMult : E_scope.
-Infix "==" := point_eq_dec (no associativity, at level 70) : E_scope.
+Infix "*" := scalarMult : E_scope.
\ No newline at end of file
diff --git a/src/Spec/EdDSA.v b/src/Spec/EdDSA.v
index 3decae6a7..8a48f4dea 100644
--- a/src/Spec/EdDSA.v
+++ b/src/Spec/EdDSA.v
@@ -6,6 +6,7 @@ Require Import Crypto.Util.WordUtil.
 Require Bedrock.Word.
 Require Coq.ZArith.Znumtheory Coq.ZArith.BinInt.
 Require Coq.Numbers.Natural.Peano.NPeano.
+Require Crypto.CompleteEdwardsCurve.CompleteEdwardsCurveTheorems.
 
 Coercion Word.wordToNat : Word.word >-> nat.
 
@@ -54,6 +55,8 @@ Section EdDSA.
   Notation secretkey := (Word.word b) (only parsing).
   Notation publickey := (Word.word b) (only parsing).
   Notation signature := (Word.word (b + b)) (only parsing).
+  Let point_eq_dec : forall P Q, {P = Q} + {P <> Q} := CompleteEdwardsCurveTheorems.point_eq_dec.
+  Local Infix "==" := point_eq_dec (at level 70) : E_scope .
 
   (* TODO: proofread curveKey and definition of n *)
   Definition curveKey (sk:secretkey) : nat :=
@@ -82,4 +85,4 @@ Section EdDSA.
     end
     end
     end%E.
-End EdDSA.
+End EdDSA.
\ No newline at end of file