Skip to content

Admitted subgoals are described as unfocused subgoals #13475

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom
Closed
Nils-Lauermann opened this issue Nov 25, 2020 · 3 comments · Fixed by rocq-prover/vsrocq#184
Closed

Admitted subgoals are described as unfocused subgoals #13475

Nils-Lauermann opened this issue Nov 25, 2020 · 3 comments · Fixed by rocq-prover/vsrocq#184
Labels
resolved: moved Moved to another bug / issue tracker.

Comments

@Nils-Lauermann
Copy link

Description of the problem

Admitting a subgoal and then closing all other subgoals will lead to the message:

There are unfocused goals.

I found this rather confusing as I tried to focus these goals but wasn't able to.

See for example:

Lemma add_zero x:
    x + 0 = x.
Proof.
    induction x.
    - admit.
    - cbn. auto.

Coq Version

The Coq Proof Assistant, version 8.12.0 (October 2020)
compiled on Oct 9 2020 14:54:23 with OCaml 4.09.1
@Zimmi48
Copy link
Member

Zimmi48 commented Nov 25, 2020

Hum, are you really observing this behavior with Coq 8.12.0?? I just tested this code with that version and I get:

No more subgoals, but there are some goals you gave up:

0 + 0 = 0

You need to go back and solve them.

@fakusb
Copy link
Contributor

fakusb commented Nov 25, 2020

It seems to be a vscoq bug.

@Zimmi48
Copy link
Member

Zimmi48 commented Nov 25, 2020

OK, please report here then: https://github.com/coq-community/vscoq/issues/

@Zimmi48 Zimmi48 closed this as completed Nov 25, 2020
@Zimmi48 Zimmi48 added the resolved: moved Moved to another bug / issue tracker. label Nov 25, 2020
fakusb added a commit to fakusb/vscoq that referenced this issue Nov 25, 2020
@fakusb
fix rocq-prover/rocq#13475
d539e73
@fakusb fakusb mentioned this issue Nov 25, 2020
Merged
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
resolved: moved Moved to another bug / issue tracker.
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

Give more informative goal message on shelved/admitted goals fakusb/vscoq
3 participants
@Zimmi48 @fakusb @Nils-Lauermann