From 0ab98d3380033b58162015656f435ae90b936856 Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Thu, 2 Mar 2017 10:58:28 -0500 Subject: make 8.5 happy --- src/Spec/WeierstrassCurve.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'src/Spec') diff --git a/src/Spec/WeierstrassCurve.v b/src/Spec/WeierstrassCurve.v index 87b5bcffd..eebc79df4 100644 --- a/src/Spec/WeierstrassCurve.v +++ b/src/Spec/WeierstrassCurve.v @@ -62,7 +62,7 @@ Module W. | ∞, _ => coordinates P2 | _, ∞ => coordinates P1 end) _. - Next Obligation. exact (Pre.add_onCurve _ _ (proj2_sig _) (proj2_sig _)). Qed. + Next Obligation. apply (Pre.add_onCurve _ _ (proj2_sig _) (proj2_sig _)). Qed. Fixpoint mul (n:nat) (P : point) : point := match n with -- cgit v1.2.3