The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

Mihai ANDRIES wrote:
> Probably one of the main problems in CoqIDE is the naming of the 
> intermediate variables.
> Although i always name my variables to keep the code easier to reuse, 
> i have no control (or at least i don't know how to control) the naming 
> of the intermediate variables, which result after applying a specific 
> tactic.
>
> It seems that the names of variables' type influence the naming 
> algorithm used in CoqIDE.
> For instance, i wanted to change the name of a type from 
> EvaluationArith to aeval, i made all the necessary changes in the 
> code, and proof's execution failed because the names of intermediate 
> variables have changed. My "apply det_ArithEval with (E:=E) (a:=e)." 
> is no longer valid.

You can avoid this problem by writing highly automated proof scripts, 
where you almost always accept Coq's default name generation but write 
tactics that are agnostic to name choices.  That is, pattern-matching 
binds names locally only, within what are conceptually single proof steps.

(Your example above sounds like it might even work well with plain [eauto].)