Stream: Coq users

Topic: Controlling the output of Show Proof


view this post on Zulip Alexander Gryzlov (Nov 04 2020 at 19:26):

I want to debug a complex SSR rewrite rule by inspecting the proof term before and after its application to see which individual steps were applied. However the proof terms are several k lines long and Show Proof starts replacing the output by ... at some particular nesting depth, hiding some of the latter steps. Is there a way to force it to spit out the full term without shortening?

view this post on Zulip Alexander Gryzlov (Nov 04 2020 at 19:28):

I'm on 8.12 by the way.

view this post on Zulip Pierre-Marie Pédrot (Nov 04 2020 at 19:43):

Have you tried the "Printing Depth" option?

view this post on Zulip Gaëtan Gilbert (Nov 04 2020 at 19:50):

there's no way to go higher than the default depth AFAIK

view this post on Zulip Alexander Gryzlov (Nov 04 2020 at 22:36):

yeah it doesn't look like changing it to more than 50 affects anything

view this post on Zulip Alexander Gryzlov (Nov 04 2020 at 22:36):

is there maybe another way to export the term in a middle of a proof?

view this post on Zulip Paolo Giarrusso (Nov 04 2020 at 23:01):

For a closing proof, there is abstract.

view this post on Zulip Paolo Giarrusso (Nov 04 2020 at 23:02):

It doesn't sound like the proof is closing, but you could e.g. "rewrite (_ : a = b) by abstract rewrite ...". Probably painful.

view this post on Zulip Alexander Gryzlov (Nov 04 2020 at 23:08):

hmm thanks


Last updated: Feb 01 2023 at 11:04 UTC