coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: "Soegtrop, Michael" <michael.soegtrop AT intel.com>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: RE: [Coq-Club] module "best practices"?
Date: Fri, 24 Aug 2018 14:49:19 +0000
Accept-language: de-DE, en-US
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=michael.soegtrop AT intel.com; spf=Pass smtp.mailfrom=michael.soegtrop AT intel.com; spf=None smtp.helo=postmaster AT mga11.intel.com
Ironport-phdr: 9a23:33s13BcsW9s0S8FOfRWDp92plGMj4u6mDksu8pMizoh2WeGdxcS8Yh7h7PlgxGXEQZ/co6odzbaO7Oa4ASQp2tWoiDg6aptCVhsI2409vjcLJ4q7M3D9N+PgdCcgHc5PBxdP9nC/NlVJSo6lPwWB6nK94iQPFRrhKAF7Ovr6GpLIj8Swyuu+54Dfbx9HiTahY75+Ngm6oRnMvcQKnIVuLbo8xAHUqXVSYeRWwm1oJVOXnxni48q74YBu/SdNtf8/7sBMSar1cbg2QrxeFzQmLns65Nb3uhnZTAuA/WUTX2MLmRdVGQfF7RX6XpDssivms+d2xSeXMdHqQb0yRD+v6bpgRh31hycdLzM38H/ZhNFsjKxVoxyhqR5ww4/Ib46aO/RzZb/dcsgeSGZdQspdSy5MD4WhZIUPFeoBOuNYopHzq1UTqhuxGwasBP/1yj9Pnn/6xbAx3eMgEQ7a3AwvBcwBsHDaoN7oM6oSVOG1w7XIzTrZcfxW3S3x6JPPch8/rvGMQahwcc3JyUQ0FgPFiEmQppLhPz+PyusNtG2b4vNmWOmyhWAnrARxrSKuxscqkoTJiYMVykzE9SVk24k5P8G3SEl+YdK8EZtQsT2aOJVyQs84Xm5npiA3waAFt56jZCUG1ZAqywDFZ/GHc4WE+BLuWPiLLTp8in9pYK+zihe8/ES6xODxWNO43EhEoydBiNXAq3MA2wLL5sSaS/Zw+l2t1SiP2g3c8O1IP1o4mbfYJpI9xLM7i4Advl7ZHiDsnUX7lK+WeVsg+uiv8+nnZ7rmqYWBO4NpkA3+M6IumtChDuQ8KAQBQ2+b+eGk2L3i+032XqlKg+UrnqTdrpzWP8QWq66jDwJVzIov8RKyAjm+3NQdh3YHLVZFeBydj4juPlHDOPX4DfajjFSsijhk2fTGMqf6ApXKMHfDn6vhfax6605E0wczzNZf545KBbEFOv78RkjxtNnAAh8jLwO02/rnCMl61o4GRW2PBbaZPLrOvl+M++IgOPKBZJQVuTb4M/gq/eTijX4/mV8HfKmmx4EbaH6iHqcuH0LMK3Hrm5IKFXoAlgs4Vu3jzlOYG3YHbHGrGqk4+zsTCYS8DI6FSJr705Kb2yLuVKZRa29aEFeUVT/Ndo6EUvoIImrGJ85qkjUJUf66TIIuyQuprCf7zaZqKqzf/ShO5sGr78R8++CGzUJ6zjdzFcnIizjcHVExpXsBQnoN5I46pEV8zlmZ1q0h2q5ZE8Be47VCVQJobMeAndw/MMj7X0f6RvnMUEyvG4z0ADctQ9Z3yNgLMR4kRoeSyyvb1i/vOIc70ryGAJttrfDZ0HGofoB8zWrL0O8qiFx0GsY=

Dear David, Anders, Samuel,

> > 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!

I created the feature request: https://github.com/coq/coq/issues/8317

With this all "quirks" from Samuel's post would be solved.

Best regards,

Michael

Intel Deutschland GmbH
Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
Tel: +49 89 99 8853-0, www.intel.de
Managing Directors: Christin Eisenschmid, Christian Lamprechter
Chairperson of the Supervisory Board: Nicole Lau
Registered Office: Munich
Commercial Register: Amtsgericht Muenchen HRB 186928

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