The Coq mailing list

[AUGER Cédric <sedrikov AT gmail.com>]

Le Tue, 9 Oct 2012 12:01:00 +0200,
Arnaud Spiwack 
<aspiwack AT lix.polytechnique.fr>
 a écrit :

> > 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?
> >
> 
> None. It's just simpler this way (for now). It's true that it makes
> the naming of existential variables worse, but it's not like you can
> control those that exist in the background, so side effect or not, as
> long as the names are generated, they will look bad.
> 
> 
> Arnaud

Of course they looks bad, but avoiding this side effect could help in
understanding mechanics. If existentials change each time you
undo/redo, it is hard to figure who was who. For teaching purpouse, it
is good to have some deterministic generation name also.