The Coq mailing list

[Bas Spitters <spitters AT cs.kun.nl>]

Dear all,

How do I make a Coercion from Type?
The following works.
        Definition TYPE := Type.
        Inductive pair: Type
           := neg : Prop -> pair
             | pos : TYPE -> pair. 
        Coercion pos : TYPE >-> pair.


But if I try to do this directly, it is not allowed:
        Inductive pair: Type
            := neg : Prop -> pair
            | pos : Type -> pair. 
        Coercion pos : Type >-> pair.

        Toplevel input, characters 91-95
        > Coercion pos : Type >-> pair.
        >                            ^^^^
        Syntax error: [vernac:class_rawexpr] expected after ':' (in     
[vernac:gallina_ext])

Is there a reason for this? Should I use a different notation?

Thanks in advance.

Best,

Bas