coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Module Include leads to duplicate type class instances

From: Ralf Jung <jung AT mpi-sws.org>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Module Include leads to duplicate type class instances
Date: Fri, 16 Dec 2016 09:50:29 +0100
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=jung AT mpi-sws.org; spf=Pass smtp.mailfrom=jung AT mpi-sws.org; spf=None smtp.helo=postmaster AT hera.mpi-klsb.mpg.de
Ironport-phdr: 9a23:AdnZbRc0Y8keZMeDEEN1bQBnlGMj4u6mDksu8pMizoh2WeGdxc28YR7h7PlgxGXEQZ/co6odzbGH6Oa/ASdZus7J8ChbNscTB1ld0YRetjdjKfDGIHWzFOTtYS0+EZYKf35e1Fb/D3JoHt3jbUbZuHy44G1aMBz+MQ1oOra9QdaK3Izkn9y1rpbUekBDgCe3SbJ0NhS/6wvL5ecMho43EK81xFPrv31HM7BU2GVnDVeLnlPn+dz2+4RspXcD88k9/tJNBP2pN58zSqZVWWwr

Hi,

>> it
>> seems like it's actually searching for "X.foo" in one go, and there
>> could be multiple modules X that it is checking here?
>
> Correct

Well, that's what I meant by merging, I guess. Or maybe it is
backtracking on what module "X" refers to.

Kind regards,
Ralf

[Coq-Club] Module Include leads to duplicate type class instances, Robbert Krebbers, 12/13/2016
- Re: [Coq-Club] Module Include leads to duplicate type class instances, Jason Gross, 12/13/2016
  - Re: [Coq-Club] Module Include leads to duplicate type class instances, Robbert Krebbers, 12/13/2016
  - Re: [Coq-Club] Module Include leads to duplicate type class instances, Ralf Jung, 12/15/2016
    - Re: [Coq-Club] Module Include leads to duplicate type class instances, Guillaume Melquiond, 12/16/2016
      - Re: [Coq-Club] Module Include leads to duplicate type class instances, Jason Gross, 12/16/2016
        
        Re: [Coq-Club] Module Include leads to duplicate type class instances, Ralf Jung, 12/16/2016
        
        Re: [Coq-Club] Module Include leads to duplicate type class instances, Jason Gross, 12/16/2016
        
        Re: [Coq-Club] Module Include leads to duplicate type class instances, Guillaume Melquiond, 12/17/2016