coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Jason Gross <jasongross9 AT gmail.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Module Include leads to duplicate type class instances
Date: Fri, 16 Dec 2016 08:36:51 +0000
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=jasongross9 AT gmail.com; spf=Pass smtp.mailfrom=jasongross9 AT gmail.com; spf=None smtp.helo=postmaster AT mail-qt0-f182.google.com
Ironport-phdr: 9a23:Q6Qcrh1o6B8oT7wwsmDT+DRfVm0co7zxezQtwd8ZsesRKPad9pjvdHbS+e9qxAeQG96KsLQb06GP6f+oGTRZp83e4DZaKN0EfiRGoPtVtjRoONSCB0z/IayiRA0BN+MGamVY+WqmO1NeAsf0ag6aiHSz6TkPBke3blItdaymUrLV2s+wzqW5/4DZSwROnju0J71ofzusqgCElMANho0qBbw20QCB9nlBYONQynlvPknCtxn578a0upVk9nID6Loa68dcXPCiLOwDRrtCAWF+Pg==

> 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

On Fri, Dec 16, 2016, 2:57 AM Guillaume Melquiond <guillaume.melquiond AT inria.fr> wrote:

On 15/12/2016 22:27, Ralf Jung wrote:

>> If you just want namespacing, try this module structure instead:
>>
>> Module Export foo1.
>> Module bar. ... End bar.
>> End foo1.
>>
>> Module Export foo2.
>> Module bar. ... End bar.
>> End foo2.
>>
>> ...
>>
>> If you also want [Import bar] to do the right thing, you can create
>> another module [bar] which [Export]s all of the inner modules [bar].
>
> So when a module Exports multiple modules with the same name, they
> somehow get magically merged? That's scary.

I am not sure how you were able to deduce that from Jason's answer, but
no, modules don't get merged.

Best regards,

Guillaume

[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