The Coq mailing list

[Arthur Azevedo de Amorim <arthur.aa AT gmail.com>]

Have you had more than one version of Coq installed/compiled on that machine?

2014-04-29 20:40 GMT+02:00 Marcus Ramos 
<mvmramos AT gmail.com>:
> Hi,
>
> Sorry for the basic question, but I can´t find the solution on my own.
>
> I compile file "Symbols.v" (using >coqc Symbols) and obtain "Symbols.vo".
> When I try to execute a file that contains the command "Require Import
> Symbols", I receive the message:
>
> Error: Compiled library Symbols.vo makes inconsistent assumptions over
> library Coq.Init.Tactics.
>
> Since Tactics in part of the Standard Library, how I am supposed to
> interpret this error message? And what do I have to do to overcome it?
>
> Thanks in advance,
> Marcus.
>
>



-- 
Arthur Azevedo de Amorim