coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Théo Zimmermann <theo AT irif.fr>
To: Coq Club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] option to disable partially qualified Require Imports
Date: Thu, 17 Sep 2020 16:57:00 +0200
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=theo AT irif.fr; spf=Pass smtp.mailfrom=theo AT irif.fr; spf=None smtp.helo=postmaster AT korolev.univ-paris7.fr
Ironport-phdr: 9a23:XtYsSRXFSlXkQkce3ZbhWnRP/brV8LGtZVwlr6E/grcLSJyIuqrYbReAt8tkgFKBZ4jH8fUM07OQ7/m/HzRcqsbZ+DBaKdoQDkFD0Z1X1yUbQ+e9QXXhK/DrayFoVO9jb3RCu0+BDE5OBczlbEfTqHDhpRQbGxH4KBYnbr+tQt2agMu4zf299IPOaAtUmjW9falyLBKrpgnNq8Uam4RvJrszxxfTvndFdOtayGB0KVmOmxrw+tq88IRs/ihNuv8t7dJMXbn/c68lUbFWETMqPnwv6sb2rxfDVwyP5nUdUmUSjBVFBhXO4Q/5UJnsrCb0r/Jx1yaGM8L4S7A0Qimi4LxwSBD0kicHNiU2/3/Rh8dtka9UuhOhpxh4w47JfIGYMed1c63Bcd8GQ2dKQ91cXDJdDIyic4QPDvIBPedGoIn7u1sOtga1CQ21CO/y1jNEmnr60Ksn2OojDA7GxhQtEN0AsHvWrNv7OqQcX/2rwqbUwjvOdO9W2S7n5YTUbhwtvfOBULRtesTR00kvEAbFg02Op4zlJTSV0fwCvGua7+plUOKglXQnqwRrrTipwMcnl47Ehp4Vyl/a8iV024c1Jce5SE51e9KkHoFQujicOoBrTcwsX3tmtzwmyr0ap5G7Zi4KxYw7yhPfafGLb5aE7g/tWeuNPTt1imxpdbOxiRi970Ws1/PxW8ep3VhKsCZIjMfBu3AD2hHQ5MWKSPVw81mg1DuL0Q3Y9+9KIUcxlaXBKp4hxKY9lpsVsUTZHy/5gl/6jKGMdkk85ueo7P7nYrP4qZ+YM494kB/xPbkzmsG5HO82MRAOUnCG9em427Dv51P1TbVFg/Esk6TVrYrWKdkVq6O6GwNZzJov5hKlAzql0NkUh2QLIVNHdR6dgIXlJlfDK+3iA/ilmVSjijJryujGPrL/BpXNKWDOkLTmfbZn7E5czBQ8zc5F65JJDLEBIezzVlbptNPCFB85Mhe0zuT9BNVzzIMSQWOPAqmHP6POqVKE++YiLuaWaIMLuDvwJOIp6v/zgXMjhFMQc6qk0YMSaH+iH/RmJ0uZYWDrgtcECWoKogo+Q/LtiFCZUD5TfXeyX6wm6jE1EoKqFZ3DSZy1gLydwCe7GYVbaXxBClCVCHvna4GEW+oXZy+JOc9gkjkEVaC7RIM71BGushX6y7t9IebO9C0Yr8Gr6N8gzOrK3To26DY8W8+ayiSGS3x+tmIOXT4/mq5l9x9T0FCGhJR4AvtvJ91W4v5TVw48M9aI0+x3DPjzQAPPONmTHgX1Cu66CC08G4pii+QFZFxwTpD71kiajniaRoQNnrnOP6Qat6fV3nz/PcF4miTHzqgvyVc8EJIWaD+Ww5Vn/g2WPLbn1kWUk6HwKfYf2zTK8Gqdi3eIvV8dSAdqUL6aG34FNBOP8YbJo3jaRrrrMowJdxNbwJ/QK7FLZJvnlwceSQ==

This is precisely what `From` is for, isn't it?
https://coq.inria.fr/refman/proof-engine/vernacular-commands.html#coq:cmd.from-require

Théo

Le jeu. 17 sept. 2020 à 16:21, Abhishek Anand
<abhishek.anand.iitg AT gmail.com> a écrit :
>
> I used to think that using disjoint logical prefixes for different
> libraries and always using fully qualified names in Require Imports would
> suffice for avoiding errors due to incorrect files being imported.
> However, it was recently pointed out to me that this is not sufficient:
> Suppose we have 2 .vo files, one with fully qualified name A.B.C and
> another with fully qualified name B.C.
> Now we suddenly have no reliable way to Import the latter file unless there
> is a way to tell `Require Import` that the name should be interpreted in a
> fully qualified manner.
> Is there a workaround for this?
>
> Thanks,
> -- Abhishek
> http://www.cs.cornell.edu/~aa755/

[Coq-Club] option to disable partially qualified Require Imports, Abhishek Anand, 09/17/2020
- Re: [Coq-Club] option to disable partially qualified Require Imports, Théo Zimmermann, 09/17/2020
- 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