diff options
| author |  Jason Gross <jagro@google.com> | 2016-06-21 17:19:35 -0700 |
|---|---|---|
| committer | Jason Gross <jagro@google.com> | 2016-06-21 17:19:35 -0700 |
| commit | 2e91656515d14d4dcdfb352d421ccff87b4d26f0 (patch) | |
| tree | 8bc48839f48cb1257ccfebb48e8b7435a57fa082 /src/CompleteEdwardsCurve | |
| parent | 2736c4487c67e2432da0c9ee6bdd4ebdc99e4090 (diff) | |
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)
Diffstat (limited to 'src/CompleteEdwardsCurve')
| -rw-r--r-- | src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v | 2 |
1 files changed, 1 insertions, 1 deletions
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. |