From 2e91656515d14d4dcdfb352d421ccff87b4d26f0 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 21 Jun 2016 17:19:35 -0700 Subject: Use Admitted, not Qed, when a proof has admit [admit] is the same as [shelve] / [give_up] in Coq 8.5. Error: Attempt to save a proof with given up goals. If this is really what you want to do, use Admitted in place of Qed. (in proof edwards_acurve_abelian_group) --- src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'src/CompleteEdwardsCurve') diff --git a/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v b/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v index bf13d5618..683addd5d 100644 --- a/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v +++ b/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v @@ -135,7 +135,7 @@ Module E. match goal with | |- _ <> 0 => admit end. match goal with | |- _ <> 0 => admit end. match goal with | |- _ <> 0 => admit end. - Qed. + Admitted. (* TODO: move to [Group] and [AbelianGroup] as appropriate *) Lemma mul_0_l : forall P, (0 * P = zero)%E. -- cgit v1.2.3