diff options
| author |  Andres Erbsen <andreser@mit.edu> | 2016-07-09 17:21:48 -0400 |
|---|---|---|
| committer | Andres Erbsen <andreser@mit.edu> | 2016-07-11 09:59:13 -0400 |
| commit | f5c1d1e55617000d79ef4bedb899f410f09d1e4f (patch) | |
| tree | 74b798e3f6c6feda8a8b6beafada724d53afff2c /src/Spec | |
| parent | 0cdb6bb7bcefc7c2f6e08123e40a54cca040de77 (diff) | |
remove field_algebra
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). |