coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] option to disable partially qualified Require Imports

From: Abhishek Anand <abhishek.anand.iitg AT gmail.com>
To: coq-club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] option to disable partially qualified Require Imports
Date: Fri, 18 Sep 2020 07:04:31 -0700
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=abhishek.anand.iitg AT gmail.com; spf=Pass smtp.mailfrom=abhishek.anand.iitg AT gmail.com; spf=None smtp.helo=postmaster AT mail-io1-f45.google.com
Ironport-phdr: 9a23:BII3WhUBDTwSk9B4PVUA+mSNcVrV8LGtZVwlr6E/grcLSJyIuqrYbByPt8tkgFKBZ4jH8fUM07OQ7/m/HzReqsje+DBaKdoQDkFD0Z1X1yUbQ+e9QXXhK/DrayFoVO9jb3RCu0+BDE5OBczlbEfTqHDhpRQbGxH4KBYnbr+tQt2agMu4zf299IPOaAtUmjW9falyLBKrpgnNq8Uam4RvJrszxxfTvndFeutayGJqKFmOmxrw+tq88IRs/ihNuv8t7dJMXbn/c68lUbFWETMqPnwv6sb2rxfDVwyP5nUdUmUSjBVFBhXO4Q/5UJnsrCb0r/Jx1yaGM8L4S7A0Qimi4LxwSBD0kicHNiU2/3/Rh8dtka9UuhOhpxh4w47JfIGYMed1c63Bcd8GQ2dKQ8BcXDFDDIyhdYsCF+UOPehaoIf9qVUArgawCxewC+700DBEmmX70Lcm3+g9EwzL2hErEdIUsHTTqdX4LLsfXvu1zKnJ1jXDb+1Z2TTg44XUdBAuu/eMUq9tesfW00YgDAPFjlSLqYzlITyV1f4BvHKd7+V6U+KglnQrqwBwojizycchkYbJhocPxVDF8SV12po6Jdq9SENiZ9OvDZRfuT2AOYRsXsMiX39nuDw8yrAetpC1cjYHxpo7yxPCavGLbYmF7x3iWeuNPTp1inJrdr27ihi98EWuxeLxWtWp3FtOsydIktrBu24M2hHR9MWKSf1w9Vqi1zaXzw3f9P1ILEQumafYK5Mt2KM8m5sSvEjZESL7mEP7h7KMeEo+4Oin8eHnb63mppCCM490jRnzMqE0lcy+BeQ0KwkOX2+G9eil2r3u8k30TK9Fjv0xlanZv5TaKtoBqqGlBA9V154v6xe5Dzi4zNQVhWcLIE5BdR6djIXkO0vCLO35APq+mVihnzdmy+jDPrL7A5XNKnbDkK3mfbZ480NT0hE8zdBe55JPCrEOPvHzVlXru9zeFBA5NRG7z/zmCNV8yoMeVnmCAqCcMKzIsF+I4vgjLPWLZI8QoDr9MeQq5+byjX8lnl8QZbWm3ZwOaHyhAvtmJ1iZbmH3j9caEWYKuxI+Q/bwhF2DVz5TfXeyULgm6jE1EoL1RbvEE4uqmfmK2DqxVsldYXkDAVSRG1/pcZ+FUrECcnTBDNVml2ktX7igUI8s1lmHsgb8x/IzJ+DU+zYYuJGl3d584eGVlBAu+hR7Cs2c1yeGSGQizTBAfCM/wK0q+R818VyEy6Ut26UFR+wW3OtAV0IBDbCZz+F+DIqvCAfIf9PMSVH/B9v6XHc+SdU+x9JIaEF4SY370kLzmhGyCrpQrISlQYQu+/uFjXf0Lsd5jX3B0ft51gh0co50LWSjw5VH2U3WDo/NnV+ekv/zJ6sZ1S/JsmyEyDjXsQ==

Because I am assuming the library's author is not dumb enough to have a
hierarchy A/B/C/**/A/B/C.v.

"not dumb" is not a good precondition for using Coq, hopefully not something we'd like to write in the Coq manual.

If the required precondition on library structure (on all Coq libraries in the world that one may ever want to import) can be spelled out in a more objective and precise way, it may be okay.

But then it might be just simpler to just implement the feature that Gaëtan mentioned.

Re: [Coq-Club] option to disable partially qualified Require Imports, (continued)
- Re: [Coq-Club] option to disable partially qualified Require Imports, Guillaume Melquiond, 09/17/2020
  - Re: [Coq-Club] option to disable partially qualified Require Imports, Ralf Jung, 09/17/2020
    - Re: [Coq-Club] option to disable partially qualified Require Imports, Gregory Malecha, 09/17/2020
    - Re: [Coq-Club] option to disable partially qualified Require Imports, Théo Zimmermann, 09/18/2020
      - Re: [Coq-Club] option to disable partially qualified Require Imports, Ralf Jung, 09/18/2020
        
        Re: [Coq-Club] option to disable partially qualified Require Imports, Théo Zimmermann, 09/18/2020
        
        Re: [Coq-Club] option to disable partially qualified Require Imports, Gaëtan Gilbert, 09/18/2020
        
        Re: [Coq-Club] option to disable partially qualified Require Imports, Guillaume Melquiond, 09/18/2020
        Re: [Coq-Club] option to disable partially qualified Require Imports, Ralf Jung, 09/18/2020
        Re: [Coq-Club] option to disable partially qualified Require Imports, Guillaume Melquiond, 09/18/2020
        Re: [Coq-Club] option to disable partially qualified Require Imports, Abhishek Anand, 09/18/2020
        
        Re: [Coq-Club] option to disable partially qualified Require Imports, Ralf Jung, 09/18/2020
        Re: [Coq-Club] option to disable partially qualified Require Imports, Andrew Appel, 09/18/2020
        Re: [Coq-Club] option to disable partially qualified Require Imports, Andrew Appel, 09/18/2020
        Re: [Coq-Club] option to disable partially qualified Require Imports, Ralf Jung, 09/18/2020
        
        Re: [Coq-Club] option to disable partially qualified Require Imports, Gaëtan Gilbert, 09/18/2020
        
        Re: [Coq-Club] option to disable partially qualified Require Imports, Guillaume Melquiond, 09/18/2020
        Re: [Coq-Club] option to disable partially qualified Require Imports, Ralf Jung, 09/18/2020
        Re: [Coq-Club] option to disable partially qualified Require Imports, Guillaume Melquiond, 09/18/2020
        Re: [Coq-Club] option to disable partially qualified Require Imports, jonikelee AT gmail.com, 09/18/2020
        
        Re: [Coq-Club] option to disable partially qualified Require Imports, Jeremy Dawson, 09/19/2020