The Coq mailing list

[Pierre Casteran <pierre.casteran AT labri.fr>]

Yes, I met the same problem while writing tutorials or material for
Lectures.
This pattern is useful for comparing various styles of definition.

Pierre

Quoting 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?