coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Jeremy Dawson <Jeremy.Dawson AT anu.edu.au>
- To: "coq-club AT inria.fr" <coq-club AT inria.fr>
- Subject: [Coq-Club] how to require file in subdirectory
- Date: Wed, 5 Feb 2020 07:00:22 +0000
- Accept-language: en-US
- 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=RrTJVrUhaM+7xpE5Zxh9GVcbIYw9xoqCJAf951oe+ww=; b=Gx7FB3Sz1hqvn/uRTatF3tXqt4JW2j8Evva4tj/eL3jI3TAWOlni9UkKoU2nrVwr9EFFo7MO31T8erF2N4fC4t92iMULgGIEEfWkEJKAfdjLTnuZMn3ZOUFuJmEvRsbeaj7rh6Yl2mjZEXDIDH1o4xSg6rL5+LTPRPIT03CLLqL9UhssGW5lgqxntm6Q/9CF9ANbU0mfNU1XwwPGCuXO+SXuIZiugORjyB5eL+K74rmqjsTQjTEXtKTcLrg14jZ3AT52BgeuZMiubPXL0GFluvU2MYC3Sq0SixhqX6O1bYJzKRQa1slSroKCRnF/tIXIYxTHm/PpwHEBCtVbP/R1uA==
- Arc-seal: i=1; a=rsa-sha256; s=arcselector9901; d=microsoft.com; cv=none; b=L3FzWXD0cWUR0O0VhlePcdEKs0g+NVZEHrNPjwCGMNfWO4BeNeX+7Bx/U6L/TSdyEK+d41iZ7I5ST2DKuYRho+9yXQ84HzL1GCk/91ihECIX1OzQebkJ45LSLBU809rIMxJoAtRfD8q6w+vZqIrShbXfz/YfjIS2WFt8sj6BN2awHFFi3ahroNB8NKNqd23+i2Z54zAQyOesrntYfUxOL4rXV+J50Oe1lez+XuDgB56yRd+QQpESltHaejaKrg+v2ds8uRyiPlOmkW5QkMxr+LApnR02YK+2/QRrspNiJsLLw+xjBy1GLxHrCzw+BCbC6S5JdMcbWEFpGEUZmy09lg==
- 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-SY3-obe.outbound.protection.outlook.com
- Ironport-phdr: 9a23:vBdByRRWgdud0XLsfBr+tCmKwNpsv+yvbD5Q0YIujvd0So/mwa6ybRyN2/xhgRfzUJnB7Loc0qyK6vymBDRLuM7a+DBaKdoQDkRD0Z1X1yUbQ+e9QXXhK/DrayFoVO9jb3RCu0+BDE5OBczlbEfTqHDhpRQbGxH4KBYnbr+tQt2agMu4zf299IPOaAtUmjW9falyLBKrpgnNq8Uam4RvJrs+xxfTonZEZ+tayX50KV+dgh3w4tu88IN5/ylfpv4s+dRMXbnmc6g9ULdVECkoP2cp6cPxqBLNVxGP5nwSUmUXlhpHHQ3I5wzkU5nyryX3qPNz1DGVMsPqQ780Xy+i77pwRx/zlCgHLT85/3rJhcF2kalWvQiupx17w47TfYGVKP9zdb7TcN8GWWZMWNtaWipcCY2+coQPFfIMM+ZGoYfgu1sAoxiwBQiwC+3gxTBFnWP20rYg3ug9DQ3KwA4tEtQTu3rUttX1M6ISXPixwqbW1zXMcfZW2Dfg44bGaB8gr+qMXbV2ccHMzkQhEx3Kjk+OpozgPzKZzOoDvHKV7up7UuKvjXUqpBt3ojiy3MsjlJTGhp8Pxl/e6CV02YA4LsC2Rk58ZN6rCppQtyeCOot3RMMiWWBotzwgxr0Io562ejUBxpc/xxPHZPGLb5KE7g//WOuTOzt0mXxodbClixqv70Ss1/XwW8aw3VpQsyZIkcTAumoT2xDN5cWLUPtw80Wn1D2SzQ7c8PtELloxlafDK54u3Lowlp0LvEnfECD4hVn6gLKPeks5+Oel5f3rYrL9qZCCLYN0jRz+Mrg1lcy4HOQ4NBUBU3KD+eSm073j4VP2T6lWjv03lanZtorWJcMGpq6lBw9V1YEj6xWlAzi619QYmGELLFNDeB2Zk4jkI17DLOziAfuin1ihki1ny+3IM7DjGJnBM2bPnKr5cbZ48UFcyQ4zzd5F55JTD7EMOPb9VVHrtNPGCx84Mxa4zej9B9RzzYMeXmSPD7SDP6PUrF+E/PwgLPSRZIMPojn9NuAp5+Tygn8hhV8dYa6p0IMLZ3C/B/RqOlmWYX7xgtgaCmoKpQo/TOnyiFKYSzJTZnCyX7g95j4hEo6mA53DFciRh+nL1yCiW5ZSe2puC1aWEH6ueZ/OE6MHbzvXKct8mBQFU6KgQskvz0f9mhX9zu9FI/DZ/zxQmZv8z99zr7nxmAs/8C0yI82CyGaLZ2hygyUFSyJw1b0p8h818UuKzaUt268QLtdU/f4cCl5mZ66Z9PRzDpXJYiyEZs2AEQz0S9O7Rzw9U5Q43o1WOhcvK5CZlhnGmhGSLfoQnr2PCoYz9/uGjXH3OoBwx2uA3bRz1gB7EPsKDnWvg+tEzyaWB4PNlBnGxY+XTvxFmRX8ryKEx2fIu1xEWgltV6mDRWoYekbdsdX+4AXFUqOqDrMkdABGzJzbJw==
Hi,
I'm trying to run a command which I was guessing should be
From tttt.TTT Require Import ssss.
but I get the error
Cannot find a physical path bound to logical path matching suffix
<> and prefix tttt.TTT.
What does this mean?
How do I use a file tttt/TTT/ssss.vo?
The documentation contains
Variant From dirpath Require qualid
(in
https://coq.inria.fr/distrib/current/refman/proof-engine/vernacular-commands.html#coq:cmdv.from-require)
What should a dirpath look like, and where is it to be found in the
documentation? (Some of these syntax constructs seem to be defined in
https://coq.inria.fr/distrib/current/refman/language/gallina-specification-language.html
but dirpath isn't - and none of them seem to be in the index)
Thanks
Jeremy
- [Coq-Club] how to require file in subdirectory, Jeremy Dawson, 02/05/2020
- Re: [Coq-Club] how to require file in subdirectory, Donald Leung, 02/05/2020
- Re: [Coq-Club] how to require file in subdirectory, Jeremy Dawson, 02/05/2020
- Re: [Coq-Club] how to require file in subdirectory, Gaëtan Gilbert, 02/05/2020
- Re: [Coq-Club] how to require file in subdirectory, Jeremy Dawson, 02/06/2020
- Re: [Coq-Club] how to require file in subdirectory, Théo Zimmermann, 02/06/2020
- Re: [Coq-Club] how to require file in subdirectory, Jeremy Dawson, 02/06/2020
- Re: [Coq-Club] how to require file in subdirectory, Ralf Jung, 02/06/2020
- Re: [Coq-Club] how to require file in subdirectory, Pierre Courtieu, 02/06/2020
- Re: [Coq-Club] how to require file in subdirectory, Jeremy Dawson, 02/07/2020
- Re: [Coq-Club] how to require file in subdirectory, Pierre Courtieu, 02/06/2020
- Re: [Coq-Club] how to require file in subdirectory, Théo Zimmermann, 02/06/2020
- Re: [Coq-Club] how to require file in subdirectory, Ralf Jung, 02/06/2020
- Re: [Coq-Club] how to require file in subdirectory, Jeremy Dawson, 02/06/2020
- Re: [Coq-Club] how to require file in subdirectory, Théo Zimmermann, 02/06/2020
- Re: [Coq-Club] how to require file in subdirectory, Jeremy Dawson, 02/05/2020
- Re: [Coq-Club] how to require file in subdirectory, Donald Leung, 02/05/2020
Archive powered by MHonArc 2.6.18.