The Coq mailing list

[Anton Trunov <anton.a.trunov AT gmail.com>]

Hi Ray,

Yet another option is to use

From Equations Require Import Equations.

This is what the manual uses at the beginning of chapter 1, see
http://github.com/mattam82/Coq-Equations/raw/master/doc/equations.pdf

Best wishes,
Anton

> On 27 Sep 2018, at 21:26, Xuanrui Qi 
> <xqi01 AT cs.tufts.edu>
>  wrote:
> 
> 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
>>> 
>