The Coq mailing list

[Adam Chlipala <adamc AT cs.berkeley.edu>]

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.