coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] module "best practices"?

From: Anders Lundstedt <a AT anderslundstedt.se>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] module "best practices"?
Date: Fri, 24 Aug 2018 15:47:29 +0200
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=a AT anderslundstedt.se; spf=Pass smtp.mailfrom=anders AT anderslundstedt.se; spf=None smtp.helo=postmaster AT mail-wm0-f53.google.com
Ironport-phdr: 9a23:oPSrqx35Sg7DiYrTsmDT+DRfVm0co7zxezQtwd8Zse0SKfad9pjvdHbS+e9qxAeQG9mDtLQc06L/iOPJYSQ4+5GPsXQPItRndiQuroEopTEmG9OPEkbhLfTnPGQQFcVGU0J5rTngaRAGUMnxaEfPrXKs8DUcBgvwNRZvJuTyB4Xek9m72/q99pHPYQhEniaxba9vJxiqsAvdsdUbj5F/Iagr0BvJpXVIe+VSxWx2IF+Yggjx6MSt8pN96ipco/0u+dJOXqX8ZKQ4UKdXDC86PGAv5c3krgfMQA2S7XYBSGoWkx5IAw/Y7BHmW5r6ryX3uvZh1CScIMb7S60/Vza/4KdxUBLniikHOT43/m/Ul8J+kr5UrQm9pxBj2YPYfJ2ZOOZ8c67bYNgURXBBXsFUVyFZHo68aZYAAPQbPeZDsoLzoUYOrR2jCgm3GOPg1CJHhmPr1qA9yessChvJ3Ao9EN0QqnTUt9H1NLoUUe+o16nI0SvMYO5K2Tvn84jHbAksrPeRVrx+dsrRzFMgFwLDjliIqIzlOSmV1uUXvGSB4epgT+SigHMkpQFpujWixMghhpPUio4Lyl3I7yZ0zJgvKdC4RkN2Z8OvHoFKuCGALYR2R9svQ2F2tyY+zb0LoZu7czILyJQj3hLeZfmHf5SR7hLtVOucLy10hH1ieLK4iBay9VavxvfgWcmz1VZGtitFkt/SuXARzxHe6MeKRuFg8ku/2TuDzQPe5v9eLU00m6fXM5shzaQxlpoXv0TDBCj2mEDugaCMcEUr5/an6/78Yrj9vJCcMZJ7hR/kMqQ1nsy/HOI4PRUVX2iH5+uzyaHj8VfiQLpUlvE2iLXWsIjGJcQHoa60GxNa0oE66xqmEzim1MkYkmIcIVJeeBOHipDpNEvULPD5C/e/mVWsny1xy/DIJL2ySqnKe3PEifLqeat3w09a0gs6i95FtLxODbRUCfT/V1Xq/PjFCBMiLwG4366zAf100I8TQ3mLH6mVK7/fvUPO/e95cLrEX5McpDuoc6tt3PXpl3JswQZML5ns5oMebTWDJtojJkyYZXT2hdJbSTUDuAYzVvfulVuOSiJea2r0RK9uv2hnWrLjNp/KQ8WWuJLExD2yRMUEb2ZKB0qXFWrue56YVvsQLjmfcJc4z240EIO5Qopk7imA8Q/3z709c7jR8ywc8I3mjJ17uraVmhY1+jh5Sc+a1jPVQg==

On Thu, Aug 23, 2018 at 10:21:24AM +0000, Soegtrop, Michael wrote:
> Maybe we should do a feature request to have the "include
> definitions in module type ascription". I guess not that many
> people are using definitions in module types, so likely it would
> break little code.

Yes please!

Some previous discussion:
https://sympa.inria.fr/sympa/arc/coq-club/2017-10/msg00036.html

RE: [Coq-Club] module "best practices"?, (continued)
- Re: [Coq-Club] module "best practices"?, Adam Chlipala, 08/21/2018
  - Re: [Coq-Club] module "best practices"?, Kevin Hamlen, 08/21/2018
    - Re: [Coq-Club] module "best practices"?, Samuel Gruetter, 08/22/2018
      - RE: [Coq-Club] module "best practices"?, Soegtrop, Michael, 08/23/2018
        
        Re: [Coq-Club] module "best practices"?, David Holland, 08/23/2018
        
        Re: [Coq-Club] module "best practices"?, Anders Lundstedt, 08/24/2018
        
        RE: [Coq-Club] module "best practices"?, Soegtrop, Michael, 08/24/2018