The Coq mailing list

[<wenruimeng AT gmail.com>]

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.