coq / vscoq

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

Bad alignment in the output of "Print Universes Subgraph" #752

Closed YaZko closed 4 weeks ago

YaZko commented 7 months ago

A minor QoL nitpick, but in the following code:

Universe u v.
Print Universes Subgraph (u v).

Vscoq displays:

Set < u
< v

while proof general displays the easier to parse aligned version:

Set < u
    < v
YaZko commented 7 months ago

Note: it actually displays it correctly in the "Problem" textbox when hovering on it, but not in the "Messages" part of the "Coq Goal" buffer.

rtetley commented 2 months ago

This is still not solved with the new pretty printing library, and is related to #835