The Coq mailing list

[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.
 

Some interesting thing would be to allow the user to name its
existentials. For instance with a "refine (f %my_hole some_arg)."
instead of a "refine (f _ some_arg)."

It would be useful indeed.
 

plus it could be nice to have a
distinction between holes that can automatically be inferred and holes
that hold for existentials, even if that does not mean much for Coq (I
think it does for the user, when you use a big refine, being able to
identify the true holes at first glance is a plus).

It's a thought.