The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

Hi Jason,

How do you want to select the goal to be shown?  Is it the only one in 
focus?  Also, I noticed the delay between the setup of __Goal and the 
display - do you want that as well, or do you want to be able to show 
the proof at any point without prior setup?  Is that what you meant when 
saying it would be nice if you didn't need the refine?

Note that you don't need the named evar creation below: "_" works in 
place of "?[__Goal2]".

Anyway, I do have a way to do this, and can tailor it per your 
description.  See 4468 for some clues.

-- Jonathan

On 01/24/2016 12:42 AM, Jason Gross wrote:
> 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