coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[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: [Coq-Club] option to disable partially qualified Require Imports
Date: Thu, 17 Sep 2020 07:19:40 -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-il1-f172.google.com
Ironport-phdr: 9a23:2AqI5RU2S5Bcx4U7wQ9MB3KJ3uLV8LGtZVwlr6E/grcLSJyIuqrYbReHt8tkgFKBZ4jH8fUM07OQ7/m/HzRcqsnc+DBaKdoQDkFD0Z1X1yUbQ+e9QXXhK/DrayFoVO9jb3RCu0+BDE5OBczlbEfTqHDhpRQbGxH4KBYnbr+tQt2agMu4zf299IPOaAtUmjW9falyLBKrpgnNq8Uam4RvJrszxxfTvndFdOtayGFoKFmOmxrw+tq88IRs/ihNuv8t7dJMXbn/c68lUbFWETMqPnwv6sb2rxfDVwyP5nUdUmUSjBVFBhXO4Q/5UJnsrCb0r/Jx1yaGM8L4S7A0Qimi4LxwSBD0kicHNiU2/3/Rh8dtka9UuhOhpxh4w47JfIGYMed1c63Bcd8GQ2dKQ8BcXDFDDIyhdYsCF+UOM+ZWoYf+ulUAswexCBK2C+/z0DJFnGP60bE43uknDArI3BYgH9ULsHnMsNj6L6cSUeGuzKnI0zrDbO5d1Cv76IfSdBAuvOyHULVqfsXKyUkvFhjFjlWOpozmJT+azOINvHKd7+V9T+6vim8nqx1+ojW0yccsj5PGhoMRylze6Sp5x4M1KMS+RUVmbtGqDIFeuDuGN4tqXMwiWWdotT4kx7MGp5O2YScHxps6yhLBZfGLbYuF7w7tWeiRPzt1i3ZodbCiixuw7EWtyu3yW8u33VtIsiZJjMfAu3MO2hHd7MWMV/Vz/kCk2TmV1gDT7PlJLlwzlarBLZ4u3Lowlp4JvUvdAyD2hUP7h7KVeEU84uWk9fjrb7H8qpKfN4J4kBzyP6Uvl8ClHOg1MBYCUm6G8uqmzrLj51f2QLBSg/02jKbZtJfaKNwepqGjAg9V1p8v6xe7Dzu7ydgYk2QLIVBbdB6dgIjpPFbOIP/8DfihmVijjDBrx/XeMr3gBJXCMGTDna//cbph70NQ0gk+wNBF655JC7wMIej/VlLzudDGFhM5Nha7w+fjCNVzzIMeXmePD7eDP6zJsV+I5/kvI+mSa48WojryMf4l6OTojXAkg1MdfKip3YcYaH2jEfRmJl+WYXvogtsbDWgKuQ8+QPTwiFKeST5Te2qyX6Uk6z4nD4KmFJ7PSZypgLycxyi2BYZWZ2BDClCUC3jkbYSEW/EWaCKTOMBtiDIEVaLyA7MmgBqprUrxz6dtZr7f/TRdvpb+3vB04ffSnFc872onId6a1jSkRWF1hWMFRHcf2ql5rQQpw12D0LN4jv8eHNpa4f8PUwYmOrbTyuV7D5b5XQeXLYTBc0qvXtjzWWJ5ddk22dJbOx8sSeXntQjK2m+RO5FQkrWKAJIu9aeFhir+Is98zzDN06xz1gB6EPsKDnWvg+tEzyaWH5TAyhzLmKOjdKBa1ynIpj/akDi++XpAWQs1ap3rGHASYkyM84b870LGCr6qUPEpa1Qbj8GFLaROZ5viilAUHPo=

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