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:56:45 +0000
Authentication-results: mail3-smtp-sop.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-f175.google.com
Ironport-phdr: 9a23:p5bqVxYsKncN3LMo0RBWHSv/LSx+4OfEezUN459isYplN5qZoM25bnLW6fgltlLVR4KTs6sC0LuN9f+4EjVbud6oizMrSNR0TRgLiMEbzUQLIfWuLgnFFsPsdDEwB89YVVVorDmROElRH9viNRWJ+iXhpTEdFQ/iOgVrO+/7BpDdj9it1+C15pbffxhEiCCzbL52Ihi6twfcutUZjYd/JKs91gbCr2dVdehR2W5mP0+YkQzm5se38p5j8iBQtOwk+sVdT6j0fLk2QKJBAjg+PG87+MPktR/YTQuS/XQcSXkZkgBJAwfe8h73WIr6vzbguep83CmaOtD2TawxVD+/4apnVAPkhSEaPDM/7WrZiNF/jLhDrR2uqRxwwY7abo+WOvRjYK3SYcgXSnBdUstLTSFNHp+wYokJAuEcPehYtY79p14WoBW6HwasH+TvyjlVjXH3x6061P8hERrb1wEnHdIBqm/UrNLzNKcdS+C1y7LIzS7HYv5N1jf97ZLHchElof2WQb1wds/RxFApGgjYjVuQsZToMy2J2ukJqWSW7OptWfixh2I6qgx9uCWjy8Ush4TPm4kb0ErL9T9jz4YwPdC4SFB0YdqjEJZIsiGVLYp2Qsc7T2FxpCY21qQKuZCmcCUIyJkr3RHfa/uAc4iH5hLsSvydLit/hHJgYL6/hhCy/la8yuDkSMW4zFJHojBGn9TMrHwByQHf58mdRvdg/Eqs2S6D1wXJ5eFFJUA0m7DbK5kkwrMolJocq1/DHijwmEX5lq+WcV4k+vOs5un8bbXmo4WTN45wig3kLqsuncm/DfwiMgcSR2ib5fi81Lr78ELlR7VKl+Q6nbXdsJDHPssWvbW5Ag9Q0oY78RmzFTam0NICnXkGNl1JYhyHj5K6c23Jdfv/FLK0h0mmuDZt3fHPeLP7UbvXKX2Wsr76erA1xFRb0xF7mdJW/JVSBasGO+mickD0vd3cSBQ+NlrnkK7cFNxh29ZGCiq0CaiDPfaKvA==

Closer to the latter than the former. The only way to make it so that a bunch of modules named [X] all get imported when you [Import X] is to create yet another fresh module named [X] and make it so that this module exports all of the constants of the other modules [X] (so when you import only this module, you get the constants from all of them).

On Fri, Dec 16, 2016, 3:50 AM Ralf Jung <jung AT mpi-sws.org> wrote:

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