The Coq mailing list

[Ilmārs Cīrulis <ilmars.cirulis AT gmail.com>]

Thank you, Michael.

Most probably you're right. Usually I use Linux (it's on my computer). When I will use Windows version again, I will check what's the problem.

On Wed, Apr 1, 2015 at 2:05 PM, Soegtrop, Michael <michael.soegtrop AT intel.com> wrote:

Dear Cirulis,

 

Coq 8.5 compiles Gallina to native code, so it requires a working native code Ocaml compiler. On Linux it should work, if you compiled it from sources. On Windows this might become tricky. If you are using Windows, please let me know.

 

Best regards,

 

Michael

 

 

From: coq-club-request AT inria.fr [mailto:coq-club-request AT inria.fr] On Behalf Of Ilmars Cirulis
Sent: Wednesday, April 01, 2015 12:12 PM
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] The compile in Coq 8.5beta

 

I had the similar error yesterday, too.

 

 

On Thu, Mar 26, 2015 at 1:22 PM, 盛枫 <fsheng1990 AT 163.com> wrote:

Hello everyone,

I use the latest version of Coq: Coq 8.5beta. When I compile a file named Util.v, it will yeild the following messages and files:

Message: "Running: coqc -I "E:\Coq4MDE" "E:\Coq4MDE\Util.v" 2>&1";

Files:

.Util.aux

Util.glob

Util.v.d

 

it could not produce the Util.vo. And when I import the Util in another file, it occurs an error "Error: Cannot find library Util in loadpath".

 

 

 

--

To unsubscribe reply with "Nesūti spamu, ķēmīgais rausi!" in the subject heading.

--

To unsubscribe reply with "Nesūti spamu, ķēmīgais rausi!" in the subject heading.