coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] How to make local sources take precedence over the library?

From: Robbert Krebbers <mailinglists AT robbertkrebbers.nl>
To: Coq Club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] How to make local sources take precedence over the library?
Date: Wed, 4 Sep 2019 13:17:20 +0200
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=mailinglists AT robbertkrebbers.nl; spf=Pass smtp.mailfrom=mailinglists AT robbertkrebbers.nl; spf=None smtp.helo=postmaster AT filter04.hostcontrol.com
Ironport-phdr: 9a23:vUPD4hOanEDV4GoGpyEl6mtUPXoX/o7sNwtQ0KIMzox0Ivn/rarrMEGX3/hxlliBBdydt6sezbOJ7uu7BCQp2tWoiDg6aptCVhsI2409vjcLJ4q7M3D9N+PgdCcgHc5PBxdP9nC/NlVJSo6lPwWB6nK94iQPFRrhKAF7Ovr6GpLIj8Swyuu+54Dfbx9HiTagf79+Ngi6oAfRu8UZj4ZvKrs6xwfUrHdPZ+lY335jK0iJnxb76Mew/Zpj/DpVtvk86cNOUrj0crohQ7BAAzsoL2465MvwtRneVgSP/WcTUn8XkhVTHQfI6gzxU4rrvSv7sup93zSaPdHzQLspVzmu87tnRRn1gyocKTU37H/YhdBxjKJDoRKuuRp/w5LPYIqIMPZyZ77Rcc8GSWZEWMtaSi5PDZ6mb4YXEuQPI+hYoYn+qVUAoxSxCgujC//gxD9JnXL2wa433v49HQ3a0gEtHdQDu2nUotXvM6cSVPi4wrXPzTrYdPxZxy396JTVeR4ku/GDQ6l/ftHPxkk1DAPOk1KdqYn/MDOU0uQNsm6b7+VkVeKukG4ntxpxryO1xscrkYbGnZwaykrY9SV62oY6O8a3R1Vlbt6+C5tcrSeaN49vT84kXmpmuz46x6UGtJKhYSQHyJYqywTcZvGGaYSE/BbuWP6MLTp3hH9pYrayihmo/US91OHxVNO43EtJoydKlNTHq2oD2AbJ6sedT/tw5keh1iiL1wDU8uxEL0E0la7HK5E/2L48ipUevV7DHi/xg0X2kLOZdkIi+ui08eTnZbHmqoWAOI9zjwHyKqUumsqhDuQkKgUDX3KX9fm82bDh50H0Q7RHguconqTdqJzaIN4Upq+9Aw9byIYj7BO/Ai+j0NsCnHkHKFNFeBSIj4jtOlHOO+z4DeykjlS2lzdk3OvJMaP7ApXRLXjDiqnucq1m5EFC0goz1spT55RQCr0ZOvL8RlfxtMDEDh8+KwG73+HnCMxk2owCXWKPH7SWPbjJsV6I4+IvO/ODaJUUuDb7Mfgl5uThgWU3mV8HLuGV2s48b2nwNfB7KQ3Nan31x9wFDG0ivwwkTeWshkfUAhBJYHPnZaU27DwhFMqFF4rJTI23m/TV2S66GpxQaWRHEUyXOW3vfY+JQesPci+YKMJ7iXoCUe7yGMcayRiyuVqimPJcJe3O93hd7Mq7jYQn16jojRg3sAdMIYGFyWjXFzNumWkCSiUq37pyq0Zw0EzF16wq26UFR+wW3OtAV0IBDbCZz+F+DIqsCAzAesuEUg76BNWhGi06SdQt2dgKJU16Hof610GR72+RG7YQ0oezKtkx+6PY0WL2IpwlmWzB3qMslUUlWMZFP2C8neh581qKCg==

On 9/3/19 10:59 PM, Théo Zimmermann wrote:

I strongly recommend you never use Add LoadPath. Instead, you should use a _CoqProject file containing a single -R or -Q directive.

What is the reason why one should use the -R directive, ever? Shouldn't it be deprecated in favor of -Q?

[Coq-Club] How to make local sources take precedence over the library?, Karl Crary, 09/03/2019
- Re: [Coq-Club] How to make local sources take precedence over the library?, Théo Zimmermann, 09/03/2019
  - Re: [Coq-Club] How to make local sources take precedence over the library?, Karl Crary, 09/03/2019
    - Re: [Coq-Club] How to make local sources take precedence over the library?, Théo Zimmermann, 09/03/2019
      - Re: [Coq-Club] How to make local sources take precedence over the library?, Maxime Dénès, 09/04/2019
        
        Re: [Coq-Club] How to make local sources take precedence over the library?, Théo Zimmermann, 09/04/2019
      - Re: [Coq-Club] How to make local sources take precedence over the library?, Robbert Krebbers, 09/04/2019
        
        Re: [Coq-Club] How to make local sources take precedence over the library?, Théo Zimmermann, 09/04/2019
    - Re: [Coq-Club] How to make local sources take precedence over the library?, Pierre Courtieu, 09/04/2019