The Coq mailing list

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

Thanks; that is a pretty good suggestion.  It has the downside of 
needing to commit to using a module at the point where the bad 
definition is made.  I think that reduces some of the educational value; 
I sometimes want readers to be _surprised_ when a definition doesn't 
work out. :)  I could hide the module commands, but then readers 
following along typing code from a document might get confused.  Also, 
it is unfortunate to have to introduce modules early in an introduction 
to Coq.  So, I'll still be grateful if someone has a further suggestion 
that avoids modules.

On 06/13/2012 11:30 AM, Bruno Barras wrote:
> You could use modules:
>
> Module Attempt1.
>   ...
> End Attempt1.
> Module Attempt2.
>  ...
> End Attempt2.
> ... (* now the preferred style *)
>
> That should provide more or less the same semantics as Reset, but in a 
> more structured way. Moreover, that lets you refer to older attempts 
> from the preferred style.
>
> Bruno.
>
>
> On 06/13/2012 05:17 PM, Pierre Casteran wrote:
> > 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?