The Coq mailing list

[Xuanrui Qi <xqi01 AT cs.tufts.edu>]

Hello,

Thanks to Li-yao. This is right - the documentation needs to be
updated, I think!

Best,
Ray

On Thu, 2018-09-27 at 15:24 -0400, Li-yao Xia wrote:
> 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
> >