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: Mon, 19 Sep 2016 12:15:04 -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:ogMTzRey6FcuKnVp2NITEQxjlGMj4u6mDksu8pMizoh2WeGdxc29YB7h7PlgxGXEQZ/co6odzbGH6uawBSdQu97B6ClEK8McEUddyI0/pE8JPo2sMQXDNvnkbig3ToxpdWRO2DWFC3VTA9v0fFbIo3e/vnY4ExT7MhdpdKyuQtaBx5f/6+fn8JrKJg5MmTCVYLVoLRzwox+CmNMRhN5ALaA41hvApDNsduVIyGV0bQaRmBD95cq08ZNL/CFZuvZn/MlFB/apN58kRKBVWWx1e1s+49fm4EHO

On 09/15/2016 01:23 PM, Jonathan Leivent wrote:

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

Yet more hidden semantics: in 8.6, typeclasses eauto takes an optional depth arg (like auto and eauto already do).

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