The Coq mailing list

[Thomas Braibant <thomas.braibant AT gmail.com>]

> 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.

It does not provide exactly the same semantics as Reset, if one is
inside a section right ?

Section t.
   Variable toto : tutu.
   Definition tata : ...
   Reset tata.
   Definition tata : ...
End t.

has to be translated in

Module Attempt1.
Section t.
   Variable toto : tutu.
   Definition tata : ...
End t.
End Attempt1.

Module Attempt2.
Section t.
   Variable toto : tutu.
   Definition tata : ...
End t.
End Attempt2.

which may require to copy paste a lot of context.