The Coq mailing list

[Pierre Courtieu <pierre.courtieu AT cnam.fr>]

Le Thu, 19 Apr 2007 10:34:55 +0100,
Edsko de Vries 
<devriese AT cs.tcd.ie>
 a écrit :

> 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

You should also make sure that the compiled file (.vo) is in the path.

You can do that at launch:

coqide -I <path> -I <path>

or inside coqide by the command

Add LoadPath "path".

By default the current path (the path where the current file is) is in
the path.

Cheers,
Pierre Courtieu