The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

There is not, but you can make a feature request on ProofGeneral here, or for CoqIDE here.  You could also try submitting it as a feature request against Coq itself here, perhaps for a setting that allows any specified vernacular command to be executed after every sentence.

On Thu, May 25, 2017 at 6:23 PM Éric Tanter <etanter AT dcc.uchile.cl> wrote:

Hi,

When writing a proof, one can use “Show Proof” to display the current term in the response pane. This can be really helpful.
So much that I’d like to be able to turn it on at all steps, in order to follow the step-by-step construction of the term without having to write down “Show Proof” after each dot.
I understand that in general it is not practical for efficiency reasons, but as a pedagogical tool it would be great to have so that students “see” the term being built.

Is there a way to (locally) activate “Show Proof” for each step of the term construction?

Thanks,

— Éric