Skip to content
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

Proof state should be reset when "Not in proof mode." #145

Open
varkor opened this issue Feb 20, 2018 · 0 comments · May be fixed by #146
Open

Proof state should be reset when "Not in proof mode." #145

varkor opened this issue Feb 20, 2018 · 0 comments · May be fixed by #146

Comments

@varkor
Copy link

varkor commented Feb 20, 2018

At the moment, the previous proof state continues to be displayed when we try to evaluate the proof state outside of a proof. This is a little unexpected, as the displayed proof state may have nothing to do with the current position. It'd be better if the proof state was simply removed.
varkor added a commit to varkor/vscoq that referenced this issue Feb 20, 2018
@varkor
Clear the goals when not in proof mode
93f46fc 
It can be counter-intuitive to persist goals that are no longer relevant, when not in proof mode. This clears any current goals when not in proof mode, which fixes siegebell#145.
@varkor varkor linked a pull request Feb 20, 2018 that will close this issue
Open
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

Clear the goals when not in proof mode varkor/vscoq
1 participant
@varkor