coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Cannot find a physical path bound to logical path matching suffix....

From: Pierre Courtieu <pierre.courtieu AT gmail.com>
To: Coq Club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Cannot find a physical path bound to logical path matching suffix....
Date: Wed, 09 May 2018 15:54:08 +0000
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=pierre.courtieu AT gmail.com; spf=Pass smtp.mailfrom=pierre.courtieu AT gmail.com; spf=None smtp.helo=postmaster AT mail-ot0-f175.google.com
Ironport-phdr: 9a23:Nzkd9hQbBBhc0fviGteGgcWz/9psv+yvbD5Q0YIujvd0So/mwa69bBeN2/xhgRfzUJnB7Loc0qyK6/umATRIyK3CmUhKSIZLWR4BhJdetC0bK+nBN3fGKuX3ZTcxBsVIWQwt1Xi6NU9IBJS2PAWK8TW94jEIBxrwKxd+KPjrFY7OlcS30P2594HObwlSizexfb1/IA+qoQnNq8IbnZZsJqEtxxXTv3BGYf5WxWRmJVKSmxbz+MK994N9/ipTpvws6ddOXb31cKokQ7NYCi8mM30u683wqRbDVwqP6WACXWgQjxFFHhLK7BD+Xpf2ryv6qu9w0zSUMMHqUbw5Xymp4rx1QxH0ligIKz858HnWisNuiqJbvAmhrAF7z4LNfY2ZKOZycqbbcNgHR2ROQ9xRWjRODYOybYQBD+QPM+VFoYfju1QAogCzBRW1BO711jNEmmP60K883u88EQ/GxgsgH9cWvXrOrdX6Kr0SUfqrw6LV0zjDaO5W2S3h6IjJbB8hvOyHULVoccrQ10YvDRnFgUuKpYP5ODOVy/4Ns3Sa7+V+SOKikGEnqwRrrTiuwscgkJXGhoUQyl3d8yhy3YU7JcWgRUN5btOoCoZcuz+aOodsQc4uXXtktDs4x7AGv5OwYTIEx449xxHFbvyKa4iI7QznVOaWOTp4gWhqeLO7hxqr9kig1vHwWtC60FpXrCdIksPAtn8K1xzU5ciHTuVy8l291jaI0gDf8uBEIUYqmqrHM5MswLE9moAOvUjdHiL6gkb7gLGMekk5+OWl6/zrYrD8qZ+dM490hBv+MqMrmsGnGeQ4MxYBX3KB+euizrHs4Ur5QKhQjv0qk6nWro3aKN8Upq68GQBV04Ij5wyjADeh1dQUhWMHI05deBKbk4jpPEnDL+z/DfemmlijjDNrx+3dMbD6GZXMLn3DkK/7crpn6k5czhAzzdFF6J5OBLEBOqG7Zkikn9vBRjQ9Lgb8l+3gEZB20p4UcWOJGK6Qdq3I5wym/OUqdtGNaZUPtX7WLOU/+//jkDdtgV4QZ7Okm5AQdWqkH/l7C0qcaHvoxNwGFDFZ7UIFUOX2hQjaAnZobHGoUvd5v2ljUdP0PcL4XomoxYe58mK+F5xSaHpBDwnVQ3jtfoSAHfwLbXDLe5Mzonk/TbGkDrQZ+1S2rgajkuhoK+PV/msTspexjIEotd2Wrgk78HlPN+rY02yJSDsqzGYBRjtz27wn5EIklQrF3q9/jPhVU9dU4qERXw==

Hi,

You can tell coqide where to find libraies using the -R options. But
generally proofgeneral and coqide should behave the same in terms of
options, they read them from a _CoqProject file if present, otherwise the
default paths are used.

1) how and where did you compile/install unimath?
2) Do you have several instances of unimath on your computer?

Best
Pierre

P.
Le mer. 9 mai 2018 à 15:44, José Manuel Rodriguez Caballero <
josephcmac AT gmail.com>
a écrit :

> Hello,
> I'm writing

>> Require Import UniMath.Foundations.Preamble

> in CoqIDE 8.8, but it does not work. I receive the message: Cannot find a
physical path bound to logical path matching suffix UniMath.Foundations. On
the other hand, it works with Proof General. I ask this questions, because
I want to use "Require Import ..." from other peoples, but I do not know
how to let Coq to know how to import the files.

> Thank you in advance,
> José M.

[Coq-Club] Cannot find a physical path bound to logical path matching suffix...., José Manuel Rodriguez Caballero, 05/09/2018
- Re: [Coq-Club] Cannot find a physical path bound to logical path matching suffix...., Pierre Courtieu, 05/09/2018