coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Add LoadPath in Coq 8.12.2

From: Jeremy Dawson <Jeremy.Dawson AT anu.edu.au>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: [Coq-Club] Add LoadPath in Coq 8.12.2
Date: Tue, 19 Jan 2021 23:51:40 +1100
Arc-authentication-results: i=1; mx.microsoft.com 1; spf=pass smtp.mailfrom=anu.edu.au; dmarc=pass action=none header.from=anu.edu.au; dkim=pass header.d=anu.edu.au; arc=none
Arc-message-signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=microsoft.com; s=arcselector9901; h=From:Date:Subject:Message-ID:Content-Type:MIME-Version:X-MS-Exchange-SenderADCheck; bh=7KwtdMOm1olaDZZvNJvQfiN63M8CDCfqHneckItIL/o=; b=W2GIRiDuwJ4JgGvCYk3rIeZOtO7QK+/nItOxEerxHz8G+zaIO4QisUfFbraqzk+70q9fo00rbKrL6H7zF/CAPsk0XmMr13N1gG7zxqiPnkvhRF5H1UkSYwqRSoU/rXubPty4aHe25Tga31A1/APp9KpAx67j3xIt07Ehv45KujTd3YJqYHuSXrm+QLW9tqJiDuevGrfcSJZayqHOnlhzU0HxPPNAMtb6IrRR4v+YBias3RaM5kiIjq95bac+qGW9Y/0KwSfXKM6LbNS2BF+MenBIOnJS96urbudNe7PGrgm2SZ0qVtk3dqKHkq4IJrPFQ0qbpaBgb1fMOQE8K/xepA==
Arc-seal: i=1; a=rsa-sha256; s=arcselector9901; d=microsoft.com; cv=none; b=W36bw6hV9KtfAkJDbXG81hmz++l6JuM8CAqAKz5oFSMFgggfujp+0UjWnVQolq2SMw8XO2UiwjU7RDs3FwV9XNN4UpL5ncqsqS4X7nvRWuyydZu592ojAMW5WXl9VVBsTKCJUm+pU28j+2Zq1sTM2LXgY8xOmldMk+ZZMbAUCBG5buLVewCwfWKGqtyyquO+O2hIUE0ezR/4LDoyHp+AmJaFtSm+IFiJHiRFvuhZ/l1az6Wucr6JSHAf4IZlsDXxF7A6S6v3LSDiBjbyl67AqP5peprEPgpTz7CKoxMYXQvqAHRRgYCA14yyjdWE+NcCf09Hn6mD5TLHU8mwaOlBTw==
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=Jeremy.Dawson AT anu.edu.au; spf=Pass smtp.mailfrom=Jeremy.Dawson AT anu.edu.au; spf=Pass smtp.helo=postmaster AT AUS01-ME3-obe.outbound.protection.outlook.com
Ironport-phdr: 9a23:X4wH+xDs4aiYFOGl/T0tUyQJP3N1i/DPJgcQr6AfoPdwSPX/osbcNUDSrc9gkEXOFd2Cra4d2qyP6+u8AiRAuc/H7CldNsQUFlcssoY/p0QYGsmLCEn2frbBThcRO4B8bmJj5GyxKkNPGczzNBX4q3y26iMOSF2kbVImbuv6FZTPgMupyuu854PcYxlShDq6fLh+MAi6oR/eu8ULhYZuMLs9xgfGrnZHdeld2GdkKU6Okxrm6cq84Zxu/z5Mt/498sJLTLn3cbk/QbFEFjotLno75NfstRnNTAuP4mUTX2ALmRdWAAbL8Q/3UI7pviT1quRy1i+aPdbrTb8vQjSt871rSB7zhygZMTMy7XzahdZxjKJfpxKhugB/zovJa4ybKPZyYqXQds4cSGFcXMheSjZBD5uiYYUPEuQPPuhWoIfhqFUBrBuxChKhBP/txzJSmnP6waM33uYnHArb3AIgBdUOsHHModvxKqgSS/66zKzIzD7eYf1Zwzn86JPPchAnvPqBWrZ+ftTLyUYxEgPEjk+cp4L/MDKbzeQNtG6b4vF6WuKplm4rsR9+rSWyxss2kIbJm5sYx1bZ/ip23Ig7P8e3SFJnYdG6CptQsTmXOpd4T80tQ29mtzo2xqAJt5O1fCYG1JcqyhHQZvGDbYWE/A/vWeSNLDl2mH5oZLCyihKs/EWkzuDxS8i53VdFoCdDj9LCtWgN2gTc58SbUPdx41ut1DSV2wzO9u1JIlo4mK7UJpI5zbM9koAfvVnAEyPrgkn6krGae0Y+9uS16+nqZKjtqIWGOI9ukA7+N7wjmsyhDuQ8NQgDR3SW9uqh2rH/4EH1WbJEgPI4n6XAt5DVPtoUqrS+Aw9IzoYs8BG/Dyqg0NsFh3UHNEhFeBWbj4f3J17OPPH4DfC5g1i2lzdr2uzGPrnmApXKLXjPiqvufbF460JEyQozy85Q545MB7wOPP7/QFL9uMDaAxMjLgC43+XqBM95244RQW6PB7WWMKLWsV+G/OIvJOyMaZcRtjnjMfgq+fvujH8jlVETZ6ao04AXaHe+Hvl9OUqZZ2fsjs0fHmgXowoyVvbliECaXT5Je3myR7485i08CI++EYjDQZmtjKWd0ye/A51ZfXtLCkuMEHftb4WLQe0AaCOUIs97kzwLT6KtS4E71ULmiAivgbFgN6/f/jASnZPlztl8oePJ31lm/jttSs+ZzmulTmdun2pOSSVgj45lpkko6FqZ3K1py9BRCsdU4bsdcAogOJvNicBzFMv1XCrIeMrPRVq7BNy7V2JiBuktysMDNh4uU+6piQrOinLzX+0l0oeTDZlxyZrymmDrLp8nmX/Aye8sg0RgS9YdbTT31J46zBDaAsvyq2vckq+rcaoG2yuUrjWKy3fIsU1FFgdtA/ycACIvI3DOpNG83XvsCr+jDbN7bVlo9PXac+5vR4asil9LAvD+JN7ZfmS93X+qAgqFza+Na4ysfHgB2CLaCw4PlAVBpHs=

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?

Thanks

Jeremy

[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