diff options
Diffstat (limited to 'src/Spec')
| -rw-r--r-- | src/Spec/CompleteEdwardsCurve.v | 5 |
1 files changed, 3 insertions, 2 deletions
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). |