The Coq mailing list

[Joey Dodds <jdodds AT princeton.edu>]

Does your coqc version match up with the version of coq your ide is using?

Joey

On Tue, Apr 29, 2014 at 2:41 PM, Marcus Ramos <marcus.ramos AT univasf.edu.br> wrote:

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.