The Coq mailing list

[Adam Chlipala <adam AT chlipala.net>]

Georgi Guninski wrote:
> Are lemma proved coercions considered cheating that violates Pollack
> consistency?
>    

I think the issue of coercions should be considered independently of the 
way the coercion functions are defined.

I haven't read a definition of Pollack consistency.  To me, the relevant 
question is about the proper form for displaying theorem statements, so 
that we can develop high confidence that they mean what we think they 
mean.  I don't think such a form should support implicit coercions at 
all.  (I never use coercions in theorem statements.)