The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

alexander AT math.ohio-state.edu
 wrote:
> 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?

I don't think any serious Coq users ever run Coq outside a visual 
interface like Proof General, except occasionally to test proofs of a 
line or two.  Perhaps you should just mirror this practice?