The Coq mailing list

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

Let me be a bit more precise about 2). The canonical structures engine searches for instances by looking at the pair (proj, const), where proj is the projector of the structure, and const is the head constructor of the value in that position of the structure. For const, it is limited to the following cases:

- Constants.

- Sort.

- Products (forall x, T)

- Variables (the default case)

Probably your value does not have any of the above.

Best,
Beta

On Wed, Nov 6, 2013 at 10:10 AM, Beta Ziliani <beta AT mpi-sws.org> wrote:

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