document field issue re-appearing

1 files changed, 6 insertions, 5 deletions

diff --git a/src/Spec/CompleteEdwardsCurve.v b/src/Spec/CompleteEdwardsCurve.v
index 3586e1f95..23e201405 100644
--- a/src/Spec/CompleteEdwardsCurve.v
+++ b/src/Spec/CompleteEdwardsCurve.v
@@ -30,14 +30,15 @@ Section TwistedEdwardsCurves.
 
   Definition zero : point := mkPoint (0, 1) (@Pre.zeroOnCurve _ _ _ prime_q).
   
-  (* NOTE: the two matches on P1 can probably be merged, not sure whether good idea... *)
+  Definition unifiedAdd' P1' P2' :=
+    let '(x1, y1) := P1' in
+    let '(x2, y2) := P2' in
+      (((x1*y2  +  y1*x2)/(1 + d*x1*x2*y1*y2)) , ((y1*y2 - a*x1*x2)/(1 - d*x1*x2*y1*y2))).
+
   Definition unifiedAdd (P1 P2 : point) : point :=
     let 'exist P1' pf1 := P1 in
     let 'exist P2' pf2 := P2 in
-    mkPoint
-      ( let '(x1, y1) := P1' in
-        let '(x2, y2) := P2' in
-        (((x1*y2  +  y1*x2)/(1 + d*x1*x2*y1*y2)) , ((y1*y2 - a*x1*x2)/(1 - d*x1*x2*y1*y2))))
+    mkPoint (unifiedAdd' P1' P2')
       (@Pre.unifiedAdd'_onCurve _ _ _ prime_q two_lt_q nonzero_a square_a nonsquare_d _ _ pf1 pf2).
 
   Fixpoint scalarMult (n:nat) (P : point) : point :=