The Coq mailing list

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

Alexandre Pilkiewicz wrote:
> 2011/11/14 Adam 
> Chlipala<adamc AT csail.mit.edu>:
>    
> > I'm surprised that [C2] has type [C], so I think Victor has a legitimate
> > point here.  The usual section behavior rules imply to me that [C2] should
> > be parametrized over [Other].
> >      
> No, definitions in section only generalize the Variables that are used
> in the body of the definition (or its type). When you admit the proof,
> you don't use Other, so it is not generalized. Changing this would
> break tons of codes!
>
> That being said, when defining a lemma, it would be nice to be able to
> specify which variable are "used" whether they are or not. This is
> useful when you want to accelerate compilation of your .v files by
> removing the body of all proofs and replacing them by Admitted. But
> the issue is known, and Arthur Charguéraud already proposed solution
> to it.
>    

Hm, you're right, sorry!

At some point I've seen behavior with sections where a theorem is 
decided to depend on unused section variables.  That choice seems 
entirely reasonable to me, since other approaches go against the 
intuitive idea of proof irrelevance.  That is, it is unfortunate for the 
type of the theorem to depend on the specific proof used for it, 
especially when most of the proof is found automatically.  The behavior 
I'm remembering might require an intermingling with modules/module 
types, or some other feature not used in Victor's example.