Problem With Message Window Output

[georgio]

Hello everyone

I’m facing a weird problem with the message ouptut window in coqide and VSCode.

I noticed that Coq is displaying ... instead of actual values in lines that are too long.
This issue can be replicated by interpreting the last line of this code.

Here is a screenshot

Do you think there’s some sort of configurable parameter to address this issue? I haven’t been able to find any in the documentation.

Thanks in advance!
-Georgio

[robblanco]

Hi Georgio, the Printing Depth option is probably what you want. In your code, setting it to, say, 128 before Compute prints the whole term for me. I don’t think there is a way to set the option to “infinity” so that all terms are always printed in full, though.

[georgio]

Exactly what I was looking for.

Thank you very much