Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Apply without TC inference

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Apply without TC inference


Chronological Thread 
  • 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



Archive powered by MHonArc 2.6.18.

Top of Page