aboutsummaryrefslogtreecommitdiff
path: root/src/WeierstrassCurve
diff options
context:
space:
mode:
Diffstat (limited to 'src/WeierstrassCurve')
-rw-r--r--src/WeierstrassCurve/Pre.v3
1 files changed, 1 insertions, 2 deletions
diff --git a/src/WeierstrassCurve/Pre.v b/src/WeierstrassCurve/Pre.v
index 71a970b7d..b140e95b5 100644
--- a/src/WeierstrassCurve/Pre.v
+++ b/src/WeierstrassCurve/Pre.v
@@ -51,7 +51,6 @@ Section Pre.
onCurve P1 -> onCurve P2 -> onCurve (unifiedAdd' P1 P2).
Proof.
unfold onCurve, unifiedAdd'; intros [[x1 y1]|] [[x2 y2]|] H1 H2;
- break_match; trivial; setoid_subst_rel eq; only_two_square_roots;
- field_algebra; nsatz_contradict.
+ break_match; trivial; setoid_subst_rel eq; only_two_square_roots; super_nsatz.
Qed.
End Pre.