From f5c1d1e55617000d79ef4bedb899f410f09d1e4f Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Sat, 9 Jul 2016 17:21:48 -0400 Subject: remove field_algebra --- src/Spec/CompleteEdwardsCurve.v | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) (limited to 'src/Spec') diff --git a/src/Spec/CompleteEdwardsCurve.v b/src/Spec/CompleteEdwardsCurve.v index f6db1c14f..16a1217ce 100644 --- a/src/Spec/CompleteEdwardsCurve.v +++ b/src/Spec/CompleteEdwardsCurve.v @@ -29,8 +29,9 @@ Module E. Definition coordinates (P:point) : (F*F) := proj1_sig P. (** The following points are indeed on the curve -- see [CompleteEdwardsCurve.Pre] for proof *) - Local Obligation Tactic := intros; apply Pre.zeroOnCurve - || apply (Pre.unifiedAdd'_onCurve (char_gt_2:=char_gt_2) (d_nonsquare:=nonsquare_d) + Local Obligation Tactic := intros; + apply (Pre.zeroOnCurve(a_nonzero:=nonzero_a)(char_gt_2:=char_gt_2)) || + apply (Pre.unifiedAdd'_onCurve (char_gt_2:=char_gt_2) (d_nonsquare:=nonsquare_d) (a_nonzero:=nonzero_a) (a_square:=square_a) _ _ (proj2_sig _) (proj2_sig _)). Program Definition zero : point := (0, 1). -- cgit v1.2.3