The Coq mailing list

[Enrico Tassi <enrico.tassi AT inria.fr>]

On Tue, Oct 09, 2012 at 11:56:52AM +0200, Pierre Courtieu wrote:
> Mmmh I would say it does have something to do with side effects since
> (still in v8.4) when you go back and forth in a script the existential
> variables numbers actually change. Is there any reason for that by the way?

The gory details are that the state of the prover is made by, say, 2
components. The Undo command works on one (the proof status), but the
meta counter is stored in the other. For example if you Reset Initial
the meta counters are reset correctly, since this command operates
on the data structure holding the meta counter too.

Eventually my paral-itp branch will see the light, and this annoying
behaviour of unstable meta numbers will be fixed "by side effect" ;-)

Cheers
-- 
Enrico Tassi