The Coq mailing list

[Jonathan <jonikelee AT gmail.com>]

I've been getting careless and not carefully naming all variables in a 
proof script myself.  Is there any mechanism that can help one to rework 
a proof script so that all of the variables used in tactics are not of 
the automatically-named variety?

For instance, is there some mechanism in Coq that would alter the 
automatic naming in a predictable way - say by appending a user-provided 
suffix to each automatically generated name?  A "Set Auto Naming Suffix" 
command?  Given that, I could provide some easily distinguishable suffix 
like "__" (double underscore), and rerun a script to see where it fails 
- and clean up the instances one by one.

This became a bit more important recently, as there was something 
introduced into the trunk version of Coq that slightly changed the 
automatic naming scheme in certain cases.

-- Jonathan