The Coq mailing list

[Théo Zimmermann <theo.zimmi AT gmail.com>]

Hi,

When you say "I installed", you mean "I build from source", right? What configuration options did you use? ./configure -local?

When you say "I tried to process a file", you mean a file from the theories/ folder right?

If the answer to all these questions is yes, then I've been observing the same problem when trying to improve some theories files (with Emacs/Proof-General too). I wanted to ask around what this was about but did not get to do it yet. However, not being an expert on these matters, I'm afraid I can't help further.

Best,

Théo

Le ven. 10 févr. 2017 à 16:13, Anthony Bordg <bordg.anthony AT gmail.com> a écrit :

Hi,

I installed Coq 8.6. The installation went smoothly, however I tried to process a file with CoqIDE (the "Forward one command") to check it works and I got the following error after the command "Require Export Relation_Definitions." :

"Error:
The file /home/anthony/coq-8.6/theories/Relations/Relation_Definitions.vo contains library
Coq.Relations.Relation_Definitions and not library Relation_Definitions"

It seems there is a discrepancy between physical names and logical names.

How can I fix this problem ?

Best regards

--

PhD. Anthony Bordg

postdoctoral fellow

Mathematical Institute Charles University
https://sites.google.com/site/anthonybordg/