Skip to content
New issue

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

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

Already on GitHub? # to your account

Goal printing gets rids of brackets #802

Closed
TheoWinterhalter opened this issue Jun 26, 2024 · 0 comments · Fixed by #804
Closed

Goal printing gets rids of brackets #802

TheoWinterhalter opened this issue Jun 26, 2024 · 0 comments · Fixed by #804
Labels
bug Something isn't working

Comments

@TheoWinterhalter
Copy link

It seems VSCoq doesn't pretty-print brackets like [] in goals.

For instance the following is enough:

From Coq Require Import List.
Import ListNotations.

Lemma foo (x : list nat) : [] = x.

The goal is printed like so:

x : list nat
(1 / 1)
 = x

which is quite confusing.

Screenshot 2024-06-26 at 16 32 18

I'm on the latest version of VSCoq and VSCoq server, using Coq 8.18.

@rtetley rtetley added the bug Something isn't working label Jun 27, 2024
@rtetley rtetley mentioned this issue Jun 27, 2024
# for free to join this conversation on GitHub. Already have an account? # to comment
Labels
bug Something isn't working
Projects
None yet
Development

Successfully merging a pull request may close this issue.

2 participants