The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

Hi,

Can someone explain to me how [Identity Coercion]s are used?  I can declare one easily enough, but I cannot think of a use-case.  That is, I cannot find a statement that will typecheck/run when I have declared a constant as an identity coercion, but which will fail if I have defined that constant, but not declared it as an identity coercion.  Can someone show me such a statement, or else explain to me what [Identity Coercion] is supposed to do if no such statement exists?

Thanks,

Jason