Ssreflect Users Discussion List

[Florent Hivert <>]

      Dear Georges,

Thanks for your quick answer.

On Mon, Mar 14, 2016 at 06:06:51PM +0000, Georges Gonthier wrote:
>    While the code was accepted in 8.4, I suspect it did not have the 
> intended semantics, and that Coq simply ignored the predArgType annotation 
> in the Structure declaration, as this was the case in earlier versions, and 
> that this was "fixed" in 8.5 by trying to equate the sort imposed by the 
> Record/structure code with the declared one - whence your error.

>    Thus, there are no perfect solutions; you should also probably report a 
> Coq bug.

I'm not sure what to report... It looks to me like a bug which *was* fixed. Or
else I don't quite get what you mean by "imposed by the Record/structure".

Regards,

Florent