Stream: Coq users

Topic: Show Ltac Profile's printer


view this post on Zulip Armaël Guéneau (Sep 09 2021 at 12:43):

I'm trying to use Show Ltac Profile but the fixed number of columns used by the pretty printer means that my tactic names are getting truncated a bit too much (it looks like it some cases the full path of the tactic gets printed, which is nice but doesn't help). Is there any way around that? This is somewhat frustrating, as the data's there, just not getting printed completely...

view this post on Zulip Guillaume Melquiond (Sep 09 2021 at 12:46):

This is hardcoded. You would need to change a line in Coq and recompile.

view this post on Zulip Armaël Guéneau (Sep 09 2021 at 12:49):

alright, thanks.


Last updated: Jan 28 2023 at 06:30 UTC