coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Add LoadPath in Coq 8.12.2

From: Clément Pit-Claudel <cpitclaudel AT gmail.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Add LoadPath in Coq 8.12.2
Date: Tue, 19 Jan 2021 09:44:01 -0500
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=cpitclaudel AT gmail.com; spf=Pass smtp.mailfrom=cpitclaudel AT gmail.com; spf=None smtp.helo=postmaster AT mail-qv1-f45.google.com
Ironport-phdr: 9a23:hUZvkhFU4fkO8Qi20tRoSJ1GYnF86YWxBRYc798ds5kLTJ7zr86wAkXT6L1XgUPTWs2DsrQY0ruQ6virBzdIoc7Y9ixbL9oUD15NoP5VtjRoONSCB0z/IayiRA0BN+MGamVY+WqmO1NeAsf0ag6aiHSz6TkPBke3blItdaz6FYHIksu4yf259YHNbAVUnjq9Zq55IAmroQnLucQanI9vJrwsxhfVrXdFeupbzn5sKV6Pghrw/Mi98INh/ihKp/4t68tMWrjmcqolSrBVEC4oOH0v6s3xshnDQwqP5n8CXWgTjxFFHQvL4gzkU5noqif1ufZz1yecPc3tULA7Qi+i4LtxSB/pkygIKTg0+3zKh8NqjaJbpBWhpwFjw4PRfYqYOuZycr/bcNgHQ2dKQ8RfWDFbAo6kcoUBEeQBM+ZboYfzqVQBohmxChWjCu701j9FhGX70bEm3+kvEwzL2hErEdIUsHTTqdX4LLkfUeSvy6nN0zrDae9W1i/n5ojJbhAtuO+BXbZqfsrM1EYgCQfFhUiXpIP5JzOV1/gNvHSf7+V6SOKglnAoqwVqrzigw8cjkIjJhoYPxl/Y8iV5xZ84KNulQ0F0fdCqCoFftz2GN4RoWMMiRXlltDo+x7MIt5C3YSkHxZskyhPDd/GKfJSF7xLgWeiePDp2hHNodbaiixuy70Wt1uLxW8m23VtOsCdIkdbCu3EJ2hHV98OJSeN981+/1TqT0w3f8OJJLEAumabFNpIsxqQ8m5UTvEjbACP7l1/6ga6Lekk+5OSl5Pjrbq/lq5OAMYJ/lxvwPb40msOlBOQ1KggOUHaf+eS7zLDj+Ff2QLROjvEvi6nZro3WKd0VpqO2AwJZyIkj6xG4Dzep1NQXg2MLI05CeBKCl4TpOlfOL+7kDfqnnVigjDNmy+rFM7DhGJnBMGXPnbP7cbty60NQ0A8zwspe55JQBLEBOvXzWkrpudPEFh85MhC0zPrjCNpny4MRRHyAAquCPaPdtF+H/OMvI+2WaIAJvzb9LuAp5+Tygn8hhV8dYa6p0IMLZ3C/B/RqOlmWYX7xgtgaCmoKpQo/TOnyiFKYSzJTZnCyX7g95j4hEo6mA53DFciRh+mK2z7+FZlLbEhHDEqNGDHmbdaqQfAJPQmWo8pslCAzbbm9DqQl3AyiuQuyn7F/L/bf/iQFuZ/n/Ndw7uzX0xo18GonXIymz2iRQjQszSszTDgs0fUn+BEv+hK4yaF9xsdgO5lT6vdOCFpoMJfdy6ljFYm3VF6cONiOT1miT5OtBjRjFotgke9LWF50HpCZtj6G2iOrB7EPkLnSXc4796vd2z76IMMvki+ahplktEEvR450DUPjnrR2rlGBCIvAkkHfnKGvJ/wR

On 1/19/21 7:51 AM, Jeremy Dawson wrote:
>
> Hi,
>
> I have just upgraded my operating system, which has also involved getting
> Coq 8.12.2 (December 2020)
>
> Previously I was using Coq 8.11.2
>
> The command
> Add LoadPath "../tense-lns".
> now seems to cause an error.
>
> How do I change the command to get the same behaviour?

You should use a _CoqProject file at the root of your project, with -Q and -R
options.

[Coq-Club] Add LoadPath in Coq 8.12.2, Jeremy Dawson, 01/19/2021
- Re: [Coq-Club] Add LoadPath in Coq 8.12.2, Clément Pit-Claudel, 01/19/2021
  - Re: [Coq-Club] Add LoadPath in Coq 8.12.2, Jeremy Dawson, 01/19/2021
    - Re: [Coq-Club] Add LoadPath in Coq 8.12.2, Clément Pit-Claudel, 01/19/2021
- Re: [Coq-Club] Add LoadPath in Coq 8.12.2, Yannick Forster, 01/19/2021
  - Re: [Coq-Club] Add LoadPath in Coq 8.12.2, Pierre Courtieu, 01/19/2021
    - Re: [Coq-Club] Add LoadPath in Coq 8.12.2, Jeremy Dawson, 01/20/2021
      - Re: [Coq-Club] Add LoadPath in Coq 8.12.2, Guillaume Melquiond, 01/20/2021
        
        Re: [Coq-Club] Add LoadPath in Coq 8.12.2, Jeremy Dawson, 01/20/2021
        
        Re: [Coq-Club] Add LoadPath in Coq 8.12.2, Yannick Forster, 01/20/2021
        
        Re: [Coq-Club] Add LoadPath in Coq 8.12.2, Pierre Courtieu, 01/20/2021
  - Re: [Coq-Club] Add LoadPath in Coq 8.12.2, Jeremy Dawson, 01/20/2021