The Coq mailing list

[Enrico Tassi <enrico.tassi AT inria.fr>]

On Fri, Aug 16, 2013 at 07:43:21PM -0400, Jason Gross wrote:
> 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?

IIRC it is a way to tell coq that one node in the coercion graph has 2
denotations (eg the arguments of the type constructor are scrambled).

ciao
-- 
Enrico Tassi