coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Calling things from a parent module into another module as neat as possible

From: Pierre Courtieu <pierre.courtieu AT gmail.com>
To: Coq Club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Calling things from a parent module into another module as neat as possible
Date: Wed, 6 Jun 2018 10:58:06 +0200
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=pierre.courtieu AT gmail.com; spf=Pass smtp.mailfrom=pierre.courtieu AT gmail.com; spf=None smtp.helo=postmaster AT mail-oi0-f48.google.com
Ironport-phdr: 9a23:3u7rZBVqiPqS+RTOwUEHK6l04pbV8LGtZVwlr6E/grcLSJyIuqrYYxOOt8tkgFKBZ4jH8fUM07OQ7/i9HzRYqb+681k6OKRWUBEEjchE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i764jEdAAjwOhRoLerpBIHSk9631+ev8JHPfglEnjWwba9yIRmssQndqtQdjJd/JKo21hbHuGZDdf5MxWNvK1KTnhL86dm18ZV+7SleuO8v+tBZX6nicKs2UbJXDDI9M2Ao/8LrrgXMTRGO5nQHTGoblAdDDhXf4xH7WpfxtTb6tvZ41SKHM8D6Uaw4VDK/5KpwVhTmlDkIOCI48GHPi8x/kqRboA66pxdix4LYeZyZOOZicq/Ye94RWGhPUdtLVyFZDYy8YYkAAeoPM+hbsofzuUcBoACiBQWwHu7j1iNEimP00KA8zu8vERvG3AslH98WqnrUrcv6NL0IUe+r0aLF0zLDb+5M2Tfh6YjHbA0hquyLULJocMre11MvFxnbgVmKtYPlOC6V1v4Rs2ia8eVgSPmii2Eiqw5rozivwt0ghZXOhoIQ013J8zhyzoUtJdCgVkJ3fdqpHIFTuiyaLYd6XN4uTmJytCs1ybALv4OwcjIQx5Q93RHfbuSKc4iW7RLnU+acOTJ4i2hkeLK7nhqy9kmgxvHlWsm631tHrTBJktbLtnAK2BzT7taIRuFh8Uem3DaDzwHT6udaLkAojafXNYItz7oqmpcQsUnPBDH6lFj1gaOMeUgp+fCk6+H9bbXnop+cOZV0igb7Mqk2gsy/APo3MhIUX2eF4+izyLrj/VDjQLVWj/05jLTZvYvVJcQevKG5AgtV3pw/5Ba4CjeqyM4YkmUfLFJZZBKHiJDkNE3JIPDhFPuwn1CskCpwyP3dJb3gApDNLmDZn7v7fLZ97VRcyAspwtxF6ZJUEOJJHPWmcUjo/PfcExVxZwez2qPsDMh3/oIYQ2OGRKGDZvD8q1iNs9ouLvOWacc+vyvnN/ko+ra6lX40g0UQO6KuwIELaX2lNvtjKkSdJ3Hrh4FSQi8xogMiQbmy2xW5WjlJaiP3Bvpkv2BpOMedFY7GA7uVrvmE1Sa/EIdRYzkfWF+JGHbsMY6DXqVVMX7AEopaijUBEIOZZco5zxj37V31zrNmKqzf/ShK7cu+hugw3PXakFQJzRIxD8mZ1DvQHWR9n2dNQD5uma4j8QpyzVCM1aU+iPtdR4Re

Hi,

There may be a confusion. Indeed as Sylvain said "Import" should do
the trick but you jhave to know that a *file* is always compiled as a
module by coqc. So you probably don't need to define a module
explicitely for Base. Just put it in a file called Base.v (with no
"Module Base." inside) and do "Import Base." at the top of M1 and M2
(you also need to "Require Base." and you can do both with "Require
Import Base.").

If you have a "Module Base." in Base.v then you need to "Include Base.Base.".

Hope this helps

P.

[Coq-Club] Calling things from a parent module into another module as neat as possible, Milad Ketabii, 06/06/2018
- Re: [Coq-Club] Calling things from a parent module into another module as neat as possible, Sylvain Boulmé, 06/06/2018
  - Re: [Coq-Club] Calling things from a parent module into another module as neat as possible, Milad Ketabii, 06/06/2018
    - Re: [Coq-Club] Calling things from a parent module into another module as neat as possible, Pierre Courtieu, 06/06/2018
      - Re: [Coq-Club] Calling things from a parent module into another module as neat as possible, Ralf Jung, 06/06/2018
        
        Re: [Coq-Club] Calling things from a parent module into another module as neat as possible, Pierre Courtieu, 06/06/2018
        
        Re: [Coq-Club] Calling things from a parent module into another module as neat as possible, Milad Ketabii, 06/06/2018
    - Re: [Coq-Club] Calling things from a parent module into another module as neat as possible, Stefan Monnier, 06/06/2018