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: Milad Ketabii <ketabii.math AT gmail.com>
To: coq-club AT inria.fr
Cc: Ralf Jung <jung AT mpi-sws.org>
Subject: Re: [Coq-Club] Calling things from a parent module into another module as neat as possible
Date: Wed, 6 Jun 2018 22:21:17 +1000
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=ketabii.math AT gmail.com; spf=Pass smtp.mailfrom=ketabii.math AT gmail.com; spf=None smtp.helo=postmaster AT mail-ua0-f180.google.com
Ironport-phdr: 9a23:Ow6KfxAJ0FHdT25K6VMPUyQJP3N1i/DPJgcQr6AfoPdwSPv+psbcNUDSrc9gkEXOFd2Cra4c1qyO6+jJYi8p2d65qncMcZhBBVcuqP49uEgeOvODElDxN/XwbiY3T4xoXV5h+GynYwAOQJ6tL1LdrWev4jEMBx7xKRR6JvjvGo7Vks+7y/2+94fcbglUhDexe69+IAmrpgjNq8cahpdvJLwswRXTuHtIfOpWxWJsJV2Nmhv3+9m98p1+/SlOovwt78FPX7n0cKQ+VrxYES8pM3sp683xtBnMVhWA630BWWgLiBVIAgzF7BbnXpfttybxq+Rw1DWGMcDwULs5Qiqp4bt1RxD0iScHLz85/3/Risxsl6JQvRatqwViz4LIfI2ZMfxzdb7fc9wHX2pMRsReVyJBDI2ybIUBEvQPMvpDoobnu1cDtwGzCRWwCO7tzDJDm3/43bc90+QkCQzI2w0gH9YUv3vJsd77MbkdUfyvw6bTzDXDbu5d1DD+6IfWbhAuu+qDXbNxccbLzEkgDR/FjlWLpIzqOjOazOUNs2yB4+V8UuKvjncqpgdsqTas3schkpfFip4Rx1ze9ih0wJw5KcOlREN5e9KoDZhduz2cOoBrWM0tWXtotzw/yrAeuZ60YiwKyJM/yh7acfOHcoyI7gv+VOmLPTt0nXxldK+8ihqu60Sgxer8Vs670FZOsCVJiMXDtncI1xDL68iHTOVy/lu51DqRywze7vtILEM0mKbBNZIt37w9moAOvUnAAiP6gED2g7WXdkUg9Oio8ePnYrD+q5+fKYB0lhvxPb8vmsy+G+g4NxIBX3Sb+emn273j+Ff2QLROjvEsjqbZt5XaKdwBpqGlGw9Vzpoj6xGnAji619QYhGALI05BeBKalIfkIErOIfD9DfenmVugijZrx/bcPr3gGJrBNHbDkK2yNYp6vkVb0U84yc1Vz5NSELAIZvzpCWHrs9mNKx49OgD84Ov7Ad9818tKWm+TC6WYMeXXuEOIzu0qKuiIIoQSvWCueLAe+/fygCphyhcmdq6z0M5SMSjgR6U0EwCieXPpx+w5PyIPtws6QvbtjQTbAzFWbne2Gak742NiUd70PcL4XomoxYe58mKjBJQPPzJJD1mNFTHjcIDWA65ROhLXGddol3k/bZbkS4Il0kvw5grzyr4iM+OMvyNB5cql299y6One0xo18G4sAg==

Hi Sylvain, Pierre and Ralf

Thanks for your kind reply. Sylvain was right. I had imported the file which contained the Base but not the Base as well.

enjoy your day,

Milad

On Wed, Jun 6, 2018 at 7:25 PM, Pierre Courtieu <pierre.courtieu AT gmail.com> wrote:

Correct, sorry. Include is to be discouraged most of the time I think.
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