coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Is eauto behavior desirable?

From: Jonathan Leivent <jonikelee AT gmail.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Is eauto behavior desirable?
Date: Thu, 15 Sep 2016 13:23:33 -0400
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=jonikelee AT gmail.com; spf=Pass smtp.mailfrom=jonikelee AT gmail.com; spf=None smtp.helo=postmaster AT mail-qk0-f172.google.com
Ironport-phdr: 9a23:/0T/JBfubFFb4PNH44DQkkb/lGMj4u6mDksu8pMizoh2WeGdxc29YR7h7PlgxGXEQZ/co6odzbGH6ua/BCdZuc/J8ChbNscTB1ld0YRetjdjKfDGIHWzFOTtYS0+EZYKf35e1Fb/D3JoHt3jbUbZuHy44G1aMBz+MQ1oOra9QdaK3Izkn9y1rpbUekBDgCe3SbJ0NhS/6wvL5ecMho43CKE3wwfJq30AX+lX225uORrHnRH658S9+JNu2ytVsvMlscVHVPOpLOwDUbVEAWF+YCgO78rxuEybQA==

On 09/15/2016 01:15 PM, Matthieu Sozeau wrote:

typeclasses eauto with db does not use the typeclass_instances db.

And more hidden semantics! Of course, typeclasses eauto isn't even in the refman (which is really strange, considering that Typeclasses eauto := ... is in the refman), so the whole thing is hidden, though hinted at.

-- Jonathan

[Coq-Club] Is eauto behavior desirable?, Soegtrop, Michael, 09/15/2016
- Re: [Coq-Club] Is eauto behavior desirable?, Jonathan Leivent, 09/15/2016
  - RE: [Coq-Club] Is eauto behavior desirable?, Soegtrop, Michael, 09/15/2016
    - Re: [Coq-Club] Is eauto behavior desirable?, Jonathan Leivent, 09/15/2016
      - Re: [Coq-Club] Is eauto behavior desirable?, Matthieu Sozeau, 09/15/2016
        
        Re: [Coq-Club] Is eauto behavior desirable?, Jonathan Leivent, 09/15/2016
        
        Re: [Coq-Club] Is eauto behavior desirable?, Matthieu Sozeau, 09/15/2016
        
        Re: [Coq-Club] Is eauto behavior desirable?, Jonathan Leivent, 09/15/2016
        Re: [Coq-Club] Is eauto behavior desirable?, Jonathan Leivent, 09/19/2016
        RE: [Coq-Club] Is eauto behavior desirable?, Soegtrop, Michael, 09/20/2016
        
        RE: [Coq-Club] Is eauto behavior desirable?, Soegtrop, Michael, 09/16/2016
      - RE: [Coq-Club] Is eauto behavior desirable?, Soegtrop, Michael, 09/16/2016