coq / vscoq

Visual Studio Code extension for Coq
MIT License
335 stars 68 forks source link

Goal printing gets rids of brackets #802

Closed TheoWinterhalter closed 3 months ago

TheoWinterhalter commented 3 months ago

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.