The Coq mailing list

[Enrico Tassi <enrico.tassi AT inria.fr>]

On Fri, Jun 12, 2015 at 11:42:53AM +0100, David Black wrote:
> 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 ?

CoqIDE adds the current directory (or the directory containing the file
you opened with it).  It also reads extra flags from files named like
_CoqProject (by default, you can actually configure the name).

So yes, CoqIDE may add paths to the LoadPath, and I guess they contain
an old/different copy of Notation.vo

Best,
-- 
Enrico Tassi