The Coq mailing list

[Cyril Cohen <cohen AT crans.org>]

Oh, and the reason your structure is not used during inference might come from
the fact that vanilla Coq tactics (I mean, non ssreflect tactics) are not all
canonical structure enabled (or at least it used to be the case).
Please "Print Canonical Projections" to check if your structure is registered
for the "sort" projection, and try using refine instead of Coq's apply.
Again, it would be easier to understand with a full example.
-- 
Cyril