The Coq mailing list

[Mihai ANDRIES <mihai AT andries.eu>]

Thank you for your answer, Adam.

"eapply" sure does the job in my case, but keeping the arguments for my 
simple "apply" allows me to check easier the proof by hand.
At the same time, I find that tactics like eapply and eauto obscure a little bit the way the proof is executed.
Explicitly naming the variables in a proof was taught to me as a "good practice" for beginners.

So "eapply" is more of a workaround in this case. 
Is there a reason why the naming of variables is affected by the name of the types involved in the proof ?

On 4 December 2011 19:26, Adam Chlipala <adamc AT csail.mit.edu> wrote:

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].)