When Proofs are navigated in Vscode (specifically with the step forward and backward commands) and in the presence of an opening bracket, the green zone is delimited by the opening bracket included. However, this results in erroneous subgoals displaying as described in this issue
To fix that, this PR make the green zone end just before the opening bracket (and the begin keyword) so that the Lsp server correctly answers with the subgoals following the green zone.
Alidra
commented
2 months ago
When Proofs are navigated in Vscode (specifically with the step forward and backward commands) and in the presence of an opening bracket, the green zone is delimited by the opening bracket included. However, this results in erroneous subgoals displaying as described in this issue
To fix that, this PR make the green zone end just before the opening bracket (and the
beginkeyword) so that the Lsp server correctly answers with the subgoals following the green zone.