The Coq mailing list

[Li-yao Xia <lysxia AT gmail.com>]

Hi Xuanrui,

Try

Require Import Equations.Equations.

Looking at the "Print LoadPath" output, "Equations" is the path to the 
Equations library, but that is not a path to an actual file, which 
"Require" expects.

The logical path "Equations.Equations" refers to the module 
.../user-contrib/Equations/Equations.vo which can thus be loaded.

Li-yao

On 9/27/18 3:17 PM, Xuanrui Qi wrote:
> 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