The Coq mailing list

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

Hello.

Thanks for all the answers.

When I tried to come up with a minimal example I slightly reformulated my 
definitions and the problem disappeared. So far everything seems to be 
working as advertised and I have not tried to puzzle out what exactly went 
wrong. Not a fully satisfactory situation, but at least it works.

Regards
Christian



On 06.11.2013, at 18:22, Enrico Tassi 
<enrico.tassi AT inria.fr>
 wrote:

> 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