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: Ralf Jung <jung AT mpi-sws.org>
Cc: 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 11:25:45 +0200
Authentication-results: mail3-smtp-sop.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-ot0-f170.google.com
Ironport-phdr: 9a23:afd2VxwkfSFZmeLXCy+O+j09IxM/srCxBDY+r6Qd1OIXIJqq85mqBkHD//Il1AaPAd2Graocw8Pt8InYEVQa5piAtH1QOLdtbDQizfssogo7HcSeAlf6JvO5JwYzHcBFSUM3tyrjaRsdF8nxfUDdrWOv5jAOBBr/KRB1JuPoEYLOksi7ze+/94HTbglSmDaxfa55IQmrownWqsQYm5ZpJLwryhvOrHtIeuBWyn1tKFmOgRvy5dq+8YB6/ShItP0v68BPUaPhf6QlVrNYFygpM3o05MLwqxbOSxaE62YGXWUXlhpIBBXF7A3/U5zsvCb2qvZx1S+HNsDtU7s6RSqt4LtqSB/wiScIKTg58H3MisdtiK5XuQ+tqwBjz4LRZoyeKfhwcb7Hfd4CSmVBUMReWSxPDI2/coUBEfYOMP1Er4XhvVYCsQeyCRWuCe7p1zRGhmX23ao/0+k5Cw/G3RIvH8gUsHvKsd74KqASUf2vzKnUzDXMce5W0ir65YjQcxAuv+uMXahufsbL1UYvEB7Fjk+MqYzkITyVy/8As2ee7+V6VOKvj3QrpB12ojiq38ohjJTCiIENyl3c9yh0z5w5KcCmREN7e9KpE4VcuzuHO4Z0Xs8vRXxjtjwgxb0co5G7eTAHyJQ5yB7bbPyKa42I7QjiVOaVODt4g25ldK6mixa87EStyPHwWtO70FZNqSpFnd3MuW4X2xPP7ciHT+Nx/kan2TmRywDe8uNJLE8umabGNZIswqQ8m5kNvUjZAyP7mln6gLeTdko+++io7+rnYq/hpp+ZL4J0kgD+Pbo0msylH+s0KBQBX2+G+eSmyL3j/FP2QKhRg/05l6nWqpHaJcABqqGlBA9V154v6wyjADe+zNQYgX4HIUpZdxKAlojlIk3BIPTlDfikmFmsizdqx/XePrL7GJnNL37DkK3gfbln8UJcxhAznphj4MduA7UPaNDuXEC54N7FCBARNhS1hv34E5N6zIxICkyVBarMCKLfq0WFrskoPvOQZYII8GLlKvU//fOohngkg0MccLSB0p4eaXT+FfNjdRbKKUHwi8sMRD9Z9jE1S/bn3RjbCWYKNiSCGpkk7zR+M7qISILKR4SjmruEhX7pEZhfZ2QAAVeJQy6xK9e0HswUYSfXGfdP1yQeXOH4GYAk3BCq8gT9zug/d7eGymgjrZvmkeNNyajTmBU1r2ImCs2c1ySKUzkxkDpXH3k526dwpUE7wVCGg/B1

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