The Coq mailing list

[Bruno Barras <bruno.barras AT inria.fr>]

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?


--
Bruno Barras                    Typical team - INRIA Saclay
LIX - Ecole Polytechnique       91128 Palaiseau Cedex - France
Tel: +33 1 69 33 40 57          Fax: +33 1 69 33 30 14