The Coq mailing list

[Jonas Oberhauser <s9joober AT gmail.com>]

Am 18.01.2015 um 19:48 schrieb Andrei Borac:
> Ah sorry folks, it seems making other variables "arbitrary" is indeed
> the default in Coq,

It is not. Try this on for size:

Goal forall a b n c, ....
induction n.


What will happen is that a and b will be fixed, while c will stay 
generalized.
Coq will fix the variables until the one that you mention, from left to 
right, and keep the ones after it generalized.

hope that helps,

jonas