The Coq mailing list

[Julien Narboux <jnarboux AT narboux.fr>]

There is a command "Show intros" to display the names which will be generated. It is possible to build a script which replace intros. intos named intros, a good starting point for writing such a script could be the one for indenting writen by Eelis:

https://github.com/jnarboux/corn/blob/master/tools/coqindenter

We could have also an option to prevent you from using automatically named variables (the prefix could be something like a utf8 character for space). I think this is the default behaviour in Isabelle/Isar. 

Julien

2014-06-30 21:08 GMT+02:00 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