The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

Is there a nice way to execute [Show Proof] from Ltac?  That is, I want to be able to do something like

  let G := show_proof_term in

  idtac "Some prefix" G.

or

  show_proof_term_with_prefix "Some prefix".

The best I've been able to come up with on short notice is:

Goal True /\ False.

  let G := match goal with |- ?G => G end in

  simple refine (let __Goal := _ : G in ?[__Goal2]); [ | shelve ].

  split.

  Unshelve.

  all: cycle -1.

  let G := (eval cbv delta [__Goal] in __Goal) in

  idtac "Some prefix" G.

but I'm guessing that there's something fancy I can do with named evars and [instantiate] to execute the [idtac] in the context of __Goal2, but I'm not sure what it is.  (I'm basically fine with needing the [refine] at the beginning of the proof, though it'd be nice if I didn't need it; I mostly want this so I can minimize a bug that depends on the output of [Show Proof].)

Thanks,

Jason