The Coq mailing list

[dz dz <sophiee_shao AT hotmail.com>]

> From: Adam Chlipala 
> <adamc AT cs.berkeley.edu>
> To: dz dz 
> <sophiee_shao AT hotmail.com>
> CC: 
> Coq-club AT pauillac.inria.fr
> Subject: Re: [Coq-Club] (no subject)
> Date: Thu, 19 Apr 2007 09:13:22 -0700
>
> dz dz wrote:
> > when I input "Require Import XX" the coqide show that :User error:
> > cannot find XX library in loadpath. Here XX means some coq file i
> > wrote before, it not belongs to the coq libraries.
> > Is it because I use coq under windows system? I tried put the file I
> > want to import under different directories,the command didn't work.
>
> "Require" loads compiled (.vo) files. You could compile your XX.v file
> with the command line 'coqc XX' to produce XX.vo, and then the"Require"
> should work if the .vo file is in the current directory. Otherwise, use
> the "Load" command instead.

I have tried to compile many (.v) files, but all the files can't be 
transformed to (.vo) format.I manipulated step by step as follows: open XX 
file-> select "compile"-> select "compile buffer". Then  coqide indicated 
that : compilation output: 'coqc' ¿Ú ¿Ú ¿Ú ......(with many squares) .I 
don't know what the problem is. 
I always use "Load" instead of the "Require" command , is there any 
difference between these two command? 

Best Regards,
Ying

_________________________________________________________________
Ãâ·ÑÏÂÔØ MSN Explorer:   http://explorer.msn.com/lccn