The Coq mailing list

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

On 08/10/2013 01:16 PM, Bahman Sistany wrote: I notice coq does some renaming of variables: n0, n1, ... which intuitively makes sense in this case. However, what is the general rule by which such renaming happens?  

Local variable names, like those attached to quantifiers, have no logical meaning in Coq.  They're only there to give users a convenient way of referring to objects that are actually identified internally by number.  I believe Coq is attaching the name "n" to every quantifier, and the pretty-printer is alpha renaming to help readability.