The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

Have you read Section 16.4 of CPDT?
    http://adam.chlipala.net/cpdt/

It explains the basics of path management.

On 08/07/2014 10:48 AM, 
wenruimeng AT gmail.com
 wrote:
> I was working on some project related with CompCert. It is hard for me to use
> lib file from CompCert. When I collected all the .vo file into one directory
> and import some lib file in my .v file, it shows some errors. If I use
> "Require Import compcert.cfrontend.Cshmgen.", it shows the error it is not in
> loadpath. But actually I add the loadpath of compcert/cfrontend in the
> loadpath. In another way, if I just use "Require Import Cshmgen", it gives the
> error "e/compcert/cfrontend/Cshmgen.vo contains library
> compcert.cfrontend.Cshmgen and not library Cshmgen." Is there anyone can help
> me? I struggle with this problem for a long time. It seems a loadpath config
> and lib file compiling conflict.