The Coq mailing list

[Matej Kosik <5764c029b688c1c0d24a2e97cd764f AT gmail.com>]

Hi there,

This is somewhat controversial topic.

Recently, I was speculating how to revive the "Show Tree" command:

https://coq.inria.fr/refman/Reference-Manual009.html#hevea_command219

For those proofs that conform to certain restrictions
(no nested proofs, no bullets, no "<number> : <tactic>", ...)
I think the "Show Tree" command can provide meaningful output.

The motivation is described here:
http://217.67.21.78/doc/coq/coq-8.5-hack/index.html

Whoever is interested in this kind of thing, let me know.

I know about some of the things that must be finished
(like error handling)

Ultimately, I am mostly curious about whether this (or what)
might enable me to talk about Coq proofs with people who did not study Coq 
(specifically).

At the end of the page linked above are installation instructions.

PS: big thanks to the people at Coq Coding Sprint for giving me some of the 
essentials clues
(how Coq internally represents proof scripts)