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: Ralf Jung <jung AT mpi-sws.org>
To: coq-club AT inria.fr, Pierre Courtieu <pierre.courtieu AT gmail.com>
Subject: Re: [Coq-Club] Calling things from a parent module into another module as neat as possible
Date: Wed, 6 Jun 2018 11:04:51 +0200
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 juno.mpi-klsb.mpg.de
Ironport-phdr: 9a23:PzZaYxxNlq3tNNjXCy+O+j09IxM/srCxBDY+r6Qd1O0SIJqq85mqBkHD//Il1AaPAd2Graocw8Pt8InYEVQa5piAtH1QOLdtbDQizfssogo7HcSeAlf6JvO5JwYzHcBFSUM3tyrjaRsdF8nxfUDdrWOv5jAOBBr/KRB1JuPoEYLOksi7ze+/94HTbglSmDaxfa55IQmrownWqsQYm5ZpJLwryhvOrHtIeuBWyn1tKFmOgRvy5dq+8YB6/ShItP0v68BPUaPhf6QlVrNYFygpM3o05MLwqxbOSxaE62YGXWUXlhpIBBXF7A3/U5zsvCb2qvZx1S+HNsDtU7s6RSqt4LtqSB/wiScIKTg58H3MisdtiK5XuQ+tqwBjz4LRZoyeKfhwcb7Hfd4CWGRPQMhRWSxCDI2yYYQAAOgOMvpXoYTmu1sDrwGzCRWwCO7hyDJFgGL9060g0+QmFAHLxBAuEMgKsHTasd77MLoSUea6zKLVyjjDbe5W2THy6IXTdxAhufCMUatrccvf0kkjDQTFjk+fqYH8OT6ey+cDs3CD4uZ9W++ij3Qrpxx1rzS1xcohi5PFi40Jxlzc6Cl0zoI4KcelREN/e9KoDpRduiWAO4drTM4vTWdlszsgxLIco560Zi0KxYwnxxHBb/yHdJCF4hD+VOaXJjd0nndleKq+hxqr8kigzvb8WdKu3FZPtipFncPAuW0T2BDL68iHTOVy/lu51DqS2Q3e7vtILV0wmKbBKJMsw6Q8m5UPvUjbGy/5gkT2jKuYdkU+/eio7vzqYrf7pp+aOI95kQT+MrwvmsCmGuQ5PBMOU3Kc+eSm273v5Vf5T6lSjv0qjqnZt4jXKtgcpq6gGgNazoIj6wukADq9y9QZnXwHLEpfdx6djojpPUvOIPHiAvuljVSsimQj+/eTNbr4R57JM3LrkbH7fL875VQYgDIywMpF6tp/DawbPPP+RwelrN3VFAU0dQez3vz7Cdhg/owbUGOLRKSeNfWBn0WP47cVKu2CLK0Ivjm1f/o44fHGiGc43EQCZu+ux5RBOyPwJehvP0jMOSmkudwGC2pf+1NmFLW72m3HaiZaYjOJZ4x54zg6DIy8CoKaHdKomL3ExzigWJpMaTIfUwzeITLTb4yBHsw0RmeKOMY4yW4BTbnkUJA6kxa0u12ikuc1Hq/v4iQd8Knb+p116unUz0tg9yFyCIKYy2DITGVvlCUNXzBw0K0t+UE=

Hi,

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

"Import Base.Base.", I assume. "Include" has bad side-effects like duplicating
typeclass instances and breaking coqchk.

; Ralf

> 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