coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Robbert Krebbers <mailinglists AT robbertkrebbers.nl>
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] Apply without TC inference
- Date: Wed, 27 Jul 2016 18:45:13 +0200
- Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=mailinglists AT robbertkrebbers.nl; spf=None smtp.mailfrom=mailinglists AT robbertkrebbers.nl; spf=None smtp.helo=postmaster AT smtp1.science.ru.nl
- Ironport-phdr: 9a23:XOUa1xBGHCyFQH2AWYxgUyQJP3N1i/DPJgcQr6AfoPdwSP7+rsbcNUDSrc9gkEXOFd2CrakV06yI7uuxByQp2tWoiDg6aptCVhsI2409vjcLJ4q7M3D9N+PgdCcgHc5PBxdP9nC/NlVJSo6lPwWB6kO74TNaIBjjLw09fr2zQd+KyZrqnLHss7ToICxwzAKnZr1zKBjk5S7wjeIxxbVYF6Aq1xHSqWFJcekFjUlhJFaUggqurpzopM0rxQ0L5Klkr5IIEfiiPvdwcbsNBzM/dmsx+cfDtB/ZTALJ6GFPfH8Rl09yBALP4QvmFrTrvyHwu/BmkH2fNMzyTLY7XTW587xDUhjigiodKz0j/Wvdh9ZryqRf9kHy7ydjypLZNdnGfMF1ebnQKI5CSA==
On 07/27/2016 03:51 PM, Jonathan Leivent wrote:
Even though class_apply is not documented, IMHO this is a bug. ThereThanks for the feedback. I have created a bug report:
shouldn't be a way for reflexivity in the "0=0" subgoal to alter the
other subgoal.
Note that, if one replaces reflexivity by exact eq_refl, then typeclass
inference isn't induced in that other subgoal. However, apply eq_refl
does induce the inference. And class_apply @eq_refl doesn't.
https://coq.inria.fr/bugs/show_bug.cgi?id=4969
- [Coq-Club] Apply without TC inference, Robbert Krebbers, 07/27/2016
- Re: [Coq-Club] Apply without TC inference, Robbert Krebbers, 07/27/2016
- Re: [Coq-Club] Apply without TC inference, Jonathan Leivent, 07/27/2016
- Re: [Coq-Club] Apply without TC inference, Jason Gross, 07/27/2016
- Re: [Coq-Club] Apply without TC inference, Jonathan Leivent, 07/27/2016
- Re: [Coq-Club] Apply without TC inference, Jason Gross, 07/27/2016
- Re: [Coq-Club] Apply without TC inference, Jonathan Leivent, 07/27/2016
- Re: [Coq-Club] Apply without TC inference, Jason Gross, 07/27/2016
- Re: [Coq-Club] Apply without TC inference, Jonathan Leivent, 07/27/2016
- Re: [Coq-Club] Apply without TC inference, Robbert Krebbers, 07/27/2016
- Re: [Coq-Club] Apply without TC inference, Jason Gross, 07/27/2016
- Re: [Coq-Club] Apply without TC inference, Jonathan Leivent, 07/27/2016
- Re: [Coq-Club] Apply without TC inference, Jonathan Leivent, 07/27/2016
- Re: [Coq-Club] Apply without TC inference, Jonathan Leivent, 07/27/2016
- Re: [Coq-Club] Apply without TC inference, Matthieu Sozeau, 07/27/2016
- Re: [Coq-Club] Apply without TC inference, Jonathan Leivent, 07/27/2016
- Re: [Coq-Club] Apply without TC inference, Robbert Krebbers, 07/27/2016
- Re: [Coq-Club] Apply without TC inference, Clément Pit--Claudel, 07/27/2016
- Re: [Coq-Club] Apply without TC inference, Jonathan Leivent, 07/27/2016
- Re: [Coq-Club] Apply without TC inference, Clément Pit--Claudel, 07/27/2016
- Re: [Coq-Club] Apply without TC inference, Robbert Krebbers, 07/27/2016
- Re: [Coq-Club] Apply without TC inference, Jonathan Leivent, 07/27/2016
- Re: [Coq-Club] Apply without TC inference, Matthieu Sozeau, 07/27/2016
- Re: [Coq-Club] Apply without TC inference, Jonathan Leivent, 07/27/2016
- Re: [Coq-Club] Apply without TC inference, Robbert Krebbers, 07/27/2016
Archive powered by MHonArc 2.6.18.