coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Cyril Cohen <cohen AT crans.org>
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] No global reference exists for projection value
- Date: Wed, 06 Nov 2013 14:34:20 +0100
Hi,
Christian, when you declare canonical a record where not all the fields are
named, there is no "proj" to be registered in the canonical structure table
(as
described by Beta) and it's ok because we don't want all projections to be
registered. In the case of eqType, only the "sort" matters. So unless I missed
or misunderstood something (it would be easier with the record and the value
you want to declare as canonical) you can safely ignore the warning.
Le 06/11/2013 10:18, Beta Ziliani a écrit :
> For const, it is limited to the following cases:
> […]
> - Products (forall x, T)
Actually, if I understand the code (pasted below) right, it does not work for
dependent products (and I always wondered if there was a reason for that).
Prod (_,a,b) -> (* assert (l2=[]); *)
if dependent (mkRel 1) b then raise Not_found
else lookup_canonical_conversion (proji, Prod_cs),[a;pop b]
Best,
--
Cyril
- [Coq-Club] No global reference exists for projection value, Christian Doczkal, 10/28/2013
- Re: [Coq-Club] No global reference exists for projection value, Beta Ziliani, 11/06/2013
- Re: [Coq-Club] No global reference exists for projection value, Beta Ziliani, 11/06/2013
- Re: [Coq-Club] No global reference exists for projection value, Cyril Cohen, 11/06/2013
- Re: [Coq-Club] No global reference exists for projection value, Cyril Cohen, 11/06/2013
- Re: [Coq-Club] No global reference exists for projection value, Cyril Cohen, 11/06/2013
- Re: [Coq-Club] No global reference exists for projection value, Cyril Cohen, 11/06/2013
- Re: [Coq-Club] No global reference exists for projection value, Beta Ziliani, 11/06/2013
- Re: [Coq-Club] No global reference exists for projection value, Enrico Tassi, 11/06/2013
- Re: [Coq-Club] No global reference exists for projection value / Packaged Classes, Christian Doczkal, 11/07/2013
- Re: [Coq-Club] No global reference exists for projection value, Beta Ziliani, 11/06/2013
Archive powered by MHonArc 2.6.18.