The Coq mailing list

[Edsko de Vries <devriese AT cs.tcd.ie>]

On Thu, Apr 19, 2007 at 04:45:45PM +0800, ?? ?? wrote:
> hello,
> i am a newbie with coq.
> 
> 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.

Did you compile XX? As far as I know, Require Import only opens compiled
libraries. To compile XX, open it in coqide, then select Compile ->
Compile Buffer. Then try the import again; it should work. 

Edsko