You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
First, thank you for all the hard work on the extension!
I recently updated to modern VsCoq (vscoq-language-server 2.1.0, coq 8.18, VsCoq 2.1), and I had trouble to figure out where the Ltac debugging messages are showing, typically in the following snippet:
Goal True.
idtac "Printing something".
In previous versions, there used to be a buffer for those Ltac debugging outputs, but I can't seem to find it anymore. Is it a deprecated feature, or maybe there is a more modern way to achieve a similar effect, or I just missed the place where the output would be displayed?
The text was updated successfully, but these errors were encountered:
Hi,
First, thank you for all the hard work on the extension!
I recently updated to modern VsCoq (vscoq-language-server 2.1.0, coq 8.18, VsCoq 2.1), and I had trouble to figure out where the Ltac debugging messages are showing, typically in the following snippet:
In previous versions, there used to be a buffer for those Ltac debugging outputs, but I can't seem to find it anymore. Is it a deprecated feature, or maybe there is a more modern way to achieve a similar effect, or I just missed the place where the output would be displayed?
The text was updated successfully, but these errors were encountered: