The Coq mailing list

[alexander AT math.ohio-state.edu]

Hello,

In Coq 8.3, when using the interactive mode, when one completes a proof and
types Qed. or Defined., the program outputs the steps used in the proof.  This
was a very nice feature because it allowed us to explore our way toward a 
proof
step-by-step without having to constantly manually take notes on what commands
we had issued.  In 8.4, doing proofs in interactive mode is almost useless,
unless one tediously copies every command into a separate word processor as 
one
goes.  Is there a way to turn the feature back on so that Qed/Defined lists 
the
steps we used in our proof?  Or is there some command, once a lemma is 
defined,
which will output the steps which were used?  (e.g., it would be nice if
"Check" or "Print" would do so, but neither do)

Thanks for keeping Coq such an actively developed software package :)

-Sam Alexander