coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Apply without TC inference

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. There
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.

Thanks for the feedback. I have created a bug report:

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, Robbert Krebbers, 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