The Coq mailing list

[Beta Ziliani <beta AT mpi-sws.org>]

Hi Christian,

The answer to 2) is yes, that warning means it will not be considered. The answer to one is a bit more complicated, what is the instance you're constructing?

Cheers,

Beta

On Mon, Oct 28, 2013 at 11:34 AM, Christian Doczkal <doczkal AT ps.uni-saarland.de> 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.

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