The Coq mailing list

[Arnaud Spiwack <aspiwack AT lix.polytechnique.fr>]

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