The Coq mailing list

[Marcus Ramos <marcus.ramos AT univasf.edu.br>]

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.