vscoq
vscoq copied to clipboard
Command Inspect output is missing a line break
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.