The Coq mailing list

[Bernard Hurley <bernard AT marcade.biz>]

On Wed, Apr 18, 2012 at 01:36:57PM +0200, Andrej Bauer wrote:
> >>
> 
> I am not proposing an incompatibility change, I think. I am proposing
> that the type should be honored when explicitly given. Because I
> explicitly defined that Q should map to Type, it should map to Type.
> If I asked Coq to _infer_ the type and it decided it was Prop, then I
> would have no objection. But as far as I am concerned this is a bug.
> If I define
> 
> Definition cow : Bovine := ....
> 
> then cow should be Bovine and not something else. I am tempted to file
> a bug report.
>

I've only used Coq for about a month so perhaps I don't appreciate the issues 
involved.
However it does seem reasonable to me that you should get what you ask for!

Regards,

Bernard