The Coq mailing list

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

Dear Joey,

Thanks for the reply. The versions are below:

(* For coqc *)

The Coq Proof Assistant, version 8.4pl1 (January 2013)

compiled on Jan 06 2013 16:15:15 with OCaml 4.00.1

(* For the IDE *)

The Coq Proof Assistant, version 8.4pl1 (December 2012)

Architecture win32 running Win32 operating system

Gtk version is 2.18.7

This is coqide.exe (opt is the best one for this architecture and OS)

Now I compile the file using the IDE instead of the command line and it works. However, how can I make the IDE and the coqc command in DOS compatible again?

Best Regards,

Marcus.

2014-04-29 20:53 GMT+02:00 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.