The Coq mailing list

[David Black <dtinblack AT gmail.com>]

Hi Ralf,

Apologies for not following your instructions. It looks as though it has found the file. 

However I now have the following error: Compiled library Ssreflect.ssreflect.vo makes inconsistent assumptions

over library Coq.Init.Notations

Interestingly I copied the ssreflect related files to a new folder and from the command line in the Terminal ( I am using coqtop version 8.4pl5 ) and followed your instructions and it loaded the file without any errors. Is CoqIDE automatically loading a different version of Notations than coqtop ? Is there anyway of checking ? Or is it a different problem that is causing the error ?

Kind regards,

David  

On Fri, Jun 12, 2015 at 10:59 AM, Ralf Jung <jung AT mpi-sws.org> wrote:

Hi,

> I used the following instructions in CoqIDE:
>
> Add LoadPath "/opt/local/lib/coq/user-contrib/Ssreflect/".

That's not what I suggested should work ;-)

Quoting from my first mail:
Add LoadPath "/opt/local/lib/coq/user-contrib/".

> Require Import Ssreflect.ssreflect.

Coq concatenates the paths: if you tell it to look in
"/opt/local/lib/coq/user-contrib/", and it looks for
Ssreflect.ssreflect, the "." becomes a "/" and a ".vo" is added. That's
the file it looks for.

The alternative would be to add "Ssreflect" to the Path *and* *not* do
the "Require", but you said that's what you tried first, and it did not
work.

Kind regards,
Ralf