coq-club AT inria.fr

Subject: The Coq mailing list

List archive

From: Mandy Martino <tesleft AT hotmail.com>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: [Coq-Club] Add Load Path however still can not find library
Date: Sun, 20 Dec 2015 14:55:32 +0800
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=tesleft AT hotmail.com; spf=Pass smtp.mailfrom=tesleft AT hotmail.com; spf=None smtp.helo=postmaster AT BAY004-OMC1S14.hotmail.com
Importance: Normal
Ironport-phdr: 9a23:WfsBjRaxsysjmu9KZ2liecT/LSx+4OfEezUN459isYplN5qZpcm4bnLW6fgltlLVR4KTs6sC0LqI9fi4EUU7or+/81k6OKRWUBEEjchE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i760zceF13FOBZvIaytQ8iJ35rxj7j60qaQSjsLrQL1Wal1IhSyoFeZnegtqqwmFJwMzADUqGBDYeVcyDAgD1uSmxHh+pX4p8Y7oGwD884mooRLVry/dKAlR5RZCi4nOiY7/oej4RLEVE6E4mYWemQQiBtBRQbfukLURJD05w7zsOZskAyTJ9H3S7d8DSiv9KNmRgPAiCAbMjc49Cfcjckm3/ETmw6ouxEqm92cW4qSLvcrJq4=

Hi,

martin@ubuntu:~/hilbertreborn/GeoCoq/Highschool$ coqtop

Welcome to Coq 8.4pl6 (December 2015)

Coq < Add LoadPath "/home/martin/hilbertreborn/GeoCoq/".

Require Import GeoCoq.Tarski_dev.Annexes.midpoint_theorems.

Coq <

Error: Cannot find library GeoCoq.Tarski_dev.Annexes.midpoint_theorems in loadpath

Regards,

Martin

[Coq-Club] make error for geocoq, Mandy Martino, 12/11/2015
- Re: [Coq-Club] make error for geocoq, Julien Narboux, 12/12/2015
  - [Coq-Club] Add Load Path however still can not find library, Mandy Martino, 12/20/2015
    - Re: [Coq-Club] Add Load Path however still can not find library, Abhishek Anand, 12/20/2015