diff options
Diffstat (limited to 'src/Curves/Weierstrass/Affine.v')
| -rw-r--r-- | src/Curves/Weierstrass/Affine.v | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/src/Curves/Weierstrass/Affine.v b/src/Curves/Weierstrass/Affine.v index 90bb3bdbc..3a48bf998 100644 --- a/src/Curves/Weierstrass/Affine.v +++ b/src/Curves/Weierstrass/Affine.v @@ -11,8 +11,10 @@ Module W. Program Definition opp (P:@W.point F Feq Fadd Fmul a b) : @W.point F Feq Fadd Fmul a b := match W.coordinates P return F*F+_ with | inl (x1, y1) => inl (x1, Fopp y1) - | _ => P + | inr tt => inr tt end. - Next Obligation. destruct P as [[[??]|[]]?]; cbv; trivial; fsatz. Qed. + Next Obligation. + cbv [W.coordinates]; break_match; trivial; fsatz. + Qed. End W. End W.
\ No newline at end of file |