vscoq icon indicating copy to clipboard operation
vscoq copied to clipboard

Command Inspect output is missing a line break

Open ybertot opened this issue 6 months ago • 1 comments

Inspect <n>. is supposed to display n elements, like the results of Search. If one puts an Inspect command in the middle of the script, the results is displayed in the message window, but it is not properly indented.

Here is a small reproducing example:

Definition two := 2.
Definition three := 3.
Inspect 2.

The output is two : natthree : nat in the message window, while it should be displayed on two lines.

ybertot avatar Aug 02 '24 08:08 ybertot