The Coq mailing list

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

> > Time Backtrack 94 0 0 .
> > ^^^^^^^^^^^^^^^^^^^^^^^
> Error: Navigation commands forbidden in nested commands

Hi

I first thought that you tried this command explicitely yourself,
but then from your second mail I understand that it's your
ProofGeneral that did it for you. Is that correct ?
In my version of ProofGeneral, it might be so if the emacs variable
coq-time-commands is non-nil, maybe something wrong in your config
file ? I let you check the emacs side with the other Pierre (Courtieu).

Now, concerning the Coq side, it's true that doing a "Time" on
a "navigation command" (i.e. Reset, Back, BackTo, Backtrack) is
a rather strange idea (since these commands are normally
instantaneous), but it is quite harmless, no reason to forbid it,
I've re-allowed that in the 8.4 svn branch (commmit 15365).

Apart from this particular case, please note that navigation commands
are not regular commands anymore, but special ones that can only be
used now in certain circumstances : 
 - not inside files given to coqc
 - not inside files loaded via "Load" (or via coqtop -l)
 - and indeed, not inside other nested commands such as Fail ...

The reason for these restrictions is that we now maintain an
explicit internal stack of (regular) executed commands and
associated states of the system (including the state of the
proof engine). For a Load, the stack will be grown by *one*
step (the Load itself), not recording all the inner steps.
For a coqc compilation, for efficiency we don't use this
backtracking stack at all. And for nested command such as Fail,
it's quite hard to give a sensible semantic to something like
Fail Backtrack.

In conterpart to these new restrictions, the benefit is that we
can properly say "go back N steps in the past" (Back N)
or "go back to state number N" (BackTo N) and Coq takes care
of everything, including proof states.
We don't need anymore the quite complex "Backtrack" command
(it is kept currently only for compatibility with Proof-General).

Best regards,
Pierre Letouzey