The Coq mailing list

[Christian Doczkal <doczkal AT ps.uni-saarland.de>]

Hello

I have a Coq development where I want to try the packaged structures approach 
along the lines of [1-2]. 

However, when I declare my structures as canonical I get the following 
warning:

        Warning: No global reference exists for projection value 
        let '{| sort := T |} := _UNBOUND_REL_1 in T in instance eqType of 
Equality.sort, ignoring it.

and my structures are not used during type inference. I could not find 
anything on this warning in the Coq Manual. So I have 2 Questions.

1) What can cause this kind of warning.
2) Does this warning mean that the structure/projection is not considered 
during type inference, or am I looking in the wrong place?

Any hints would be greatly appreciated. 

Regards
Christian

[1] François Garillot, Georges Gonthier, Assia Mahboubi, Laurence Rideau: 
Packaging Mathematical Structures. TPHOLs 2009:327-342
[2] Assia Mahboubi, Enrico Tassi: Canonical Structures for the Working Coq 
User. ITP 2013:19-34