Armaël Guéneau (Sep 09 2021 at 12:43): 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...
Guillaume Melquiond (Sep 09 2021 at 12:46):This is hardcoded. You would need to change a line in Coq and recompile.
Armaël Guéneau (Sep 09 2021 at 12:49):alright, thanks.
Last updated: Oct 04 2023 at 19:01 UTC