The Coq mailing list

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

This is the new error message that Coq 8.4beta2 gives when using coqc to 
process files that use commands like [Reset].  Unfortunately, I've been 
relying on such commands in CPDT <http://adam.chlipala.net/cpdt/>, for 
didactic typesetting of command sequences that would never be present in 
polished source files in "real" projects.  For instance, I will 
introduce a bad definition, work through examples showing why it is bad, 
and then [Reset] and redefine it.

Does anyone have suggestions on how to refactor to support 8.4beta2?