The Coq mailing list

[Enrico Tassi <enrico.tassi AT inria.fr>]

On Mon, Oct 28, 2013 at 11:34:35AM +0100, Christian Doczkal wrote:
> 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.

Plase post your code.

Ciao
-- 
Enrico Tassi