The Coq mailing list

[Pierre Letouzey <pierre.letouzey AT inria.fr>]

Hi 

I've finally looked again at this question of Reset commands in
compiled (or Load'ed) files. It turned out it wasn't too hard to
restore a basic support of this situation, it's now done in the
8.4 svn branch and trunk. Other navigation commands (Back,BackTo,
Backtrack) are still banned in files for the moment.

One caveat: a Reset in a compiled / loaded file will abort *all*
currently opened proofs. This is an potential incompatibility with
the interactive Reset, which now has enough knowledge to be more
selective. Anyway, I don't think this will be an issue in practice.

Btw, let me paste below my initial answer about this topic last month
(mistakenly addressed to one list member only, not to the whole list)

Best regards
Pierre Letouzey

> 
> Hi
> 
> Two quick notes on this topic :
> 
> - Instead of putting trials inside Module, it might also be interesting
>   to put them inside Module Type, this way they aren't kept in the local
>   environment afterwards, not even in qualified form.
> 
> - I tend to see the use of Reset as a kind of hack, even if I understand its
>   pedagogical interest. Also note that your files have then always been
>   unusable under coqIDE... Anyway, I acknowledge that I underestimated
>   the use of Reset when working on the backtrack layer of Coq. I'll 
> investigate
>   whether it's possible to support again some form of Reset in compiled 
> files
>   in a sane way.
>