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...
This is hardcoded. You would need to change a line in Coq and recompile.
Last updated: Jan 28 2023 at 06:30 UTC