1 files changed, 4 insertions, 1 deletions
diff --git a/src/Spec/CompleteEdwardsCurve.v b/src/Spec/CompleteEdwardsCurve.v
index 8dbfdf7b9..b7d2c0d8e 100644
--- a/src/Spec/CompleteEdwardsCurve.v
+++ b/src/Spec/CompleteEdwardsCurve.v
@@ -46,8 +46,11 @@ 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.
-\ No newline at end of file
+Infix "*" := scalarMult : E_scope.
+Infix "==" := point_eq_dec (no associativity, at level 70) : E_scope.