You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Most of the issues mentioned here are fixed, do we still want additional changes to be made?
And how do we want to handle the case where (part of) the goal is hidden and you have to add a - to get to the next subgoal?
One way of structuring proofs in Coq is to use bullets and braces.
This behavior can be enforced by
Set Default Goal Selector "!".
However, it seems that errors thrown by Coq about this are not presented to the end user, which is confusing.
Also it seems that in the presented code, indentation on the first line is stripped, which causes checkmarks to appear at wrong places.
The text was updated successfully, but these errors were encountered: