coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Weird import problem?

From: Xuanrui Qi <xqi01 AT cs.tufts.edu>
To: coq-club AT inria.fr
Subject: [Coq-Club] Weird import problem?
Date: Thu, 27 Sep 2018 14:17:35 -0500
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=xqi01 AT cs.tufts.edu; spf=None smtp.mailfrom=xqi01 AT cs.tufts.edu; spf=None smtp.helo=postmaster AT vm-delivery1.eecs.tufts.edu
Ironport-phdr: 9a23:ydjEXxWTDKtTmHeMG2YJIMdYZY3V8LGtZVwlr6E/grcLSJyIuqrYYxSCt8tkgFKBZ4jH8fUM07OQ7/i/HzRYqb+681k6OKRWUBEEjchE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i764jEdAAjwOhRoLerpBIHSk9631+ev8JHPfglEnjWwba9wIRmssQndqtQdjJd/JKo21hbHuGZDdf5MxWNvK1KTnhL86dm18ZV+7SleuO8v+tBZX6nicKs2UbJXDDI9M2Ao/8LrrgXMTRGO5nQHTGoblAdDDhXf4xH7WpfxtTb6tvZ41SKHM8D6Uaw4VDK/5KptVRTmijoINyQh/W/Ul8J+jLxVrhy9qBNxzIHab5qYNOZ8c67HYd8WWXBMU8RXWidcAo28dYwPD+8ZMOlZsonyvV0OrQGjBQmtGejh0T5IjWLx0Kw1yuQhEB3K0BE7Et0Sq3TYtsn1NLocUeCp16nE1yvMYO5L2Trk7oXDbxMvoemUUL5tf8fd1VMjGgLKg1mKt4DoMSmZ2+oPvmSD7udtVvijh3MkpgxyuDSixsYhhpPIi48T11vK7z92wJwvKt29UEN7YcCrEJ9XtyyCKYt2R9ouTHx2tyY+y70Gp4C0fDIKyZg63RLQdeKIfJST4h75SOaRPDl4hG5+eL6lmRm97FWgxvX9VsmyzllKsjJInsTCu3wRzRDe68eKRuFj8kqvwzqC2QLe5vlBIU8ulKrbL5AhwqQ3lpoWqUnCETb2mETqgKOLbUgr5vOo5/77YrX7qJ+cK5R0hhvgPaszh8yzGf44PRQWX2iH5eS806Xu8lH+QLVTl/E5jq3ZsI3BKskAva64AwpV0p455BqlDjem1s4YnXgdI15fdhKHlduhB1abK/fhSPy7nl6EkTFxxvmAMKeyLI/KKy3zjb7nZ6t8o3ddgF4j1NEHvrpfEfcdPfzvQQn8uMGOXUxxCBC93+uyUIY17YgZQ2/aWvbIYpOXikeB46cUG8fJYYYUvDjnLP18u6zlljklhFEBZu+k0YZFMCnkTMQjGF2QZD/XuvlECX0D51ZsR/eslECMTSUVanqvDfplu2MLTbm+BIKGfbiDxbyM2CDhT89IYyVKB1SND3ryZtzCVvoHc2SOP8F9iXoJWaXzE4I=

Hello all,

I appear to have run into a weird Import problem in Coq. I have
installed the "coq-equations" package using opam, but when I try to
Require Import the package:

Coq < Require Import Equations.
Toplevel input, characters 15-24:
> Require Import Equations.
> ^^^^^^^^^
Error: Unable to locate library Equations.

However, if I issue the "Print LoadPath." command, I can see that
Equations is in the load path!

Coq < Print LoadPath.
Logical Path / Physical path:
<> /home/xuanrui
<> /home/xuanrui/.opam/4.07.0/lib/coq/user-contrib
Equations /home/xuanrui/.opam/4.07.0/lib/coq/user-contrib/Equations

I also have ssreflect installed the same way, and I have no problems
importing ssreflect. I wonder what could be going wrong with Coq, or
perhaps it is a problem in the packaging of Equations?

Thanks a lot for your assistance.

-Ray

[Coq-Club] Weird import problem?, Xuanrui Qi, 09/27/2018
- Re: [Coq-Club] Weird import problem?, Li-yao Xia, 09/27/2018
  - Re: [Coq-Club] Weird import problem?, Xuanrui Qi, 09/27/2018
    - Re: [Coq-Club] Weird import problem?, Anton Trunov, 09/27/2018