coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: José Manuel Rodriguez Caballero <josephcmac AT gmail.com>
To: coq-club AT inria.fr
Subject: [Coq-Club] Cannot find a physical path bound to logical path matching suffix....
Date: Wed, 9 May 2018 15:44:08 +0200
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=josephcmac AT gmail.com; spf=Pass smtp.mailfrom=josephcmac AT gmail.com; spf=None smtp.helo=postmaster AT mail-io0-f174.google.com
Ironport-phdr: 9a23:NkvKlx2Y3RNZZr2ismDT+DRfVm0co7zxezQtwd8Zse0TKvad9pjvdHbS+e9qxAeQG9mDsLQc06L/iOPJYSQ4+5GPsXQPItRndiQuroEopTEmG9OPEkbhLfTnPGQQFcVGU0J5rTngaRAGUMnxaEfPrXKs8DUcBgvwNRZvJuTyB4Xek9m72/q99pHPbQhEniaxba9vJxiqsAvdsdUbj5F/Iagr0BvJpXVIe+VSxWx2IF+Yggjx6MSt8pN96ipco/0u+dJOXqX8ZKQ4UKdXDC86PGAv5c3krgfMQA2S7XYBSGoWkx5IAw/Y7BHmW5r6ryX3uvZh1CScIMb7S60/Vza/4KdxUBLmiCkJOT0k/m/JlsN9l7hUrA67qhFl34LYfIOYOfxjda3dZ9MaQm9BU95VWSxGGYO7dZMAAe0bMuZesonyuV8OogOiCwmrGezv0D5IhnDr3aIk0uUuCR/L0xY7EN0UtHTUqMv6NL0VUeuoy6TIzzLDb+hI1jfl6IjHbhUhruuQUr9rfsrRzFMgFwLBjlmKtYPlODaV2/0LvmOG7ORgTfqih3A7pwx1uDSixcchhpPXio4LxF3I7zh1zYQ6KNC+VUV1e8SrEIFKuCGfL4Z2Qt0tQ2VvuCsiz70Jo5+7fCwTxJQmwB7Td+WLc4aV7h/hW+udOzh4hHVieLKwgxa971KsxfH7VsmxyFpKryxFncfQtn0VyRDf9syKRuF+80qhwzqDyR7f5+9eLUwpl6fWJIYtwrsqmZoStUTDEDX2mELzjKKOdEUk/fOo5Pr/YrXmupCcMpV7hR3lP6Qhn8ywG+U4MgwUU2eH/uS80aXv/VflT7VSkv02jq7ZvYjGKsQcv661GhNa0oI+6xmkFDqmy9QZnXwfLF1fYh6Hjo7pO0vPIP/iF/u/jU6sw39XwKXNOaSkCZHQJFDClq3gdPBz8R1y0g02mPJY/BNjL7gHPf/3bXX2uMbZAQI0ITufyuzuDNFwzIRWDWCIGaKBMKjXuFSg6ecmIu3Kb4gQ7mWuY8M57uLj2Cdq0WQWerOkiMNOOSKIW89+KkDcWkLCx9IIEGMEpA07FbW4h1iLUDoVbHG3DftlumMLTbm+BIKGfbiDxaSb1X7iTJJTb2FCTFuLFCWwLtjWa7I3cCuXZ/RZvHkEWLymEdFz0BivsEr7zOIiILOLpmsXspXs0NUz7OrWx0k/

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