The Coq mailing list

[Ralf Jung <jung AT mpi-sws.org>]

Hi,

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

Great :D

> 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 ?

Uh, no idea, sorry. All I know is that this error means (as you probably
guessed already) that the version of Coq.Init.Notations that was
imported when compiling ssreflect.vo is different from the one imported
right now.

Kind regards,
Ralf