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/Experiments | |
| 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/Experiments')
0 files changed, 0 insertions, 0 deletions