coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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: Fri, 18 Sep 2020 12:48:36 +0200
- Authentication-results: mail2-smtp-roc.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:S4V2ehyW1X9BgwPXCy+O+j09IxM/srCxBDY+r6Qd2+0fIJqq85mqBkHD//Il1AaPAdyEraoawLGO++C4ACpcuMjH6ChDOLV3FDY9wf0MmAIhBMPXQWbaF9XNKxIAIcJZSVV+9Gu6O0UGUOz3ZlnVv2HgpWVKQka3OgV6PPn6FZDPhMqrye+y54fTYwJVjzahfL9+Nhq7oRjTu8UMnYdvK6k9xxXVrnBVf+ha2X5kKUickhrh58q85oJv/zhVt/k868NOTKL2crgiQ7dFFjomKWc15MPqtRnHUwSC42YXX3sVnBRVHQXL9Qn2UZjtvCT0sOp9wzSaMtbtTb8oQzSi7rxkRwHuhSwaKjM26mDXish3jKJGvBKsogF0zoDIbI2JMvd1Y7jQds0GS2VfQslRVjRBAoKiYIsJE+oBJvtTo43kq1cTsReyGQygCeXywTFKm3D2x7U33OsvEQ7E3AIuEdEAvmnKotrpL6oSTfy5wbPUwTnfc/9b2zHw45XIfBA7pvGMWKp9f9TRyU41EAPKllafqY3gPzOQyOsNqW2b4PBmVeKplmUqrB1xojixyccrkYTJh5gVylHK9SljzoY1P8S1RUhmatGrDJVerTuVN5dqQsw8WWFovj43xqEJt5O5ciUG1pQqyhDQZvKHc4aE/g/vWfuRLDp2mH5ofK+ziguv/UWuzuDxS8q53VlKoyZYktfCtm0B2wDX58WBV/Bz/V+h1C6S2w3X5exIO144mKrUJpI7w7M8i4AfvVnNEyL1gEn6krOae0E+9uWr6+nreKvqqoOfOoNulw3zMKQjl8qiCuoiKAcORXKU+eGk2b3j40L5RLJKg+U1kqneqpDaIsAbqbCnAwNPz4Yj7Re/Dym/3NQAh3YHNlNFeAmFgoTzNVHOOuj0Dfa5g1uyjDdm3+3KM7nuD5nXMHTOkLjscax85kJB0gY/0N5S6pFMBrEEOv3zW0vxtNLCDh8+Ngy52/rnCNVj2YMZQm+PA7WZMKLcsVOS6OIvOfGAZJUJtzblN/gl+/nugGclll8aZKmlxIcYaHSlHvt9OEiZenrtgtIZEWgQpAY+TerqiEeDUTFJfXqyUbg8tXkHD9eNCp6LbYSwivTV1yCiW5ZSe2puC1aWEH6ueZ/SCNkWbyfHHs/glQs2VL2kRpUk3Beo/Fvmy7dgBuvO+yNeu4i1h4s93PHaiRxnrW88NM+ayWzYCjgsxjpUFQ9z57h2pAlG8nnGybJx0q5ZD91dof1TAF9jZMzsitdiAtW3YTrvO9KASVKoWNKjUGMwVNM/hdEUMR8kRoeSyyvb1i/vOIc70ryGAJturvDf2GL2I8tjjWvA1bdkl1A8Q9AQc2O81PZy
> I've had quite weird problems in the past caused by stale .vo files being
> picked
> up by ambiguous imports, so I'd be all for a way to ensure that all imports
> are
> unambiguous. (In fact I am quite surprised that ambiguous imports exist at
> all,
> that seems quite contrary to Coq's usual design geared towards precision. No
> other language I work or worked with has ambiguous imports the way Coq does
> --
> Python, Java, C++, Rust all do not have this problem.)
With Dune, this won't be an issue anymore.
- [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
- 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, Gaëtan Gilbert, 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, Ralf Jung, 09/18/2020
- Re: [Coq-Club] option to disable partially qualified Require Imports, Ralf Jung, 09/17/2020
Archive powered by MHonArc 2.6.19+.