The Coq mailing list

[Alan Schmitt <alan.schmitt AT polytechnique.org>]

leegys AT gmail.com
 writes:

> The user's contribution library GroupTheory can be well compiled just by
> using the command 'make'.
> However, when I like to use g1.v,  I cannot pass the following line:
>
> Require Import Laws.
>
> Emacs + ProofGeneral complains as below:
>
> Error: The file ..../GroupTheory/Laws.vo contains library
> GroupTheory.Laws and not library Laws

Since you're using ProofGeneral, you could create a file
`.dir-locals.el' with the appropriate include path. For instance, if the
path where GroupTheory is install is "../foo/GroupTheory", you could say:

--8<---------------cut here---------------start------------->8---
((coq-mode . ((coq-load-path . (("../foo/GroupTheory" "GroupTheory"))))))
--8<---------------cut here---------------end--------------->8---

You can do a `C-h v coq-load-path' to know more about what this variable
means.

Hope this helps,

Alan