The Coq mailing list

[Pierre Courtieu <pierre.courtieu AT gmail.com>]

2012/10/9 Arnaud Spiwack <aspiwack AT lix.polytechnique.fr>

I have never understood the true reason to have a side effect counter
for both existentials and type universes. For me some existential
information should be stacked in order to retrieve them when taking
back, so that redoing your stuff would regenerate the same numbers, and
you could use them as names. Having a 100 lines code which contains
existentials such as %541 or universes such as (*Type 203*) is rather
ridiculous, and makes things harder to understand.

Plus people will laugh at you when you will tell them that Coq is
purely functionnal (of course such a thing won't affect pure
functionnality of Coq, but well that looks so non pure…).

This has nothing to do with side effects, really. Only with the fact that the names are generated.

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?

P.