coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Installation

From: Anthony Bordg <bordg.anthony AT gmail.com>
To: coq-club <coq-club AT inria.fr>
Subject: [Coq-Club] Installation
Date: Fri, 10 Feb 2017 16:12:52 +0100
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=bordg.anthony AT gmail.com; spf=Pass smtp.mailfrom=bordg.anthony AT gmail.com; spf=None smtp.helo=postmaster AT mail-ot0-f178.google.com
Ironport-phdr: 9a23:KD9AjBGWJagbJNnkpqT+Yp1GYnF86YWxBRYc798ds5kLTJ75p8qwAkXT6L1XgUPTWs2DsrQf2raQ4/+rBz1Ioc7Y9itdINoUD15NoP5VtjJjKfbNMVf8Iv/uYn5yN+V5f3ghwUuGN1NIEt31fVzYry76xzcTHhLiKVg9fbytScbktNmsz+2557HUZgxJgnL9PeIzf12KqlDasdBTio9/IO5lwRzQ53BMZu5+xGVyJFvVkQyqtemq+5s22iJMu/Un5oZqVr/2cOxsR7tCADtgOmYp5MrtpDHMSAKO4j0XVWBAwUkAOBTM8ByvBsS5iSD9rOcohHiX

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/

[Coq-Club] Installation, Anthony Bordg, 02/10/2017
- Re: [Coq-Club] Installation, Théo Zimmermann, 02/10/2017
  - Re: [Coq-Club] Installation, Anthony Bordg, 02/10/2017
    - Re: [Coq-Club] Installation, Christian Doczkal, 02/10/2017
- RE: [Coq-Club] Installation, Soegtrop, Michael, 02/10/2017
  - Re: [Coq-Club] Installation, Anthony Bordg, 02/10/2017