The Coq mailing list

[Gyesik Lee <leegys AT gmail.com>]

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

That is, coq wants to have the compiled file Laws.vo in another subdirectory called GroupTheory.

This is odd because g1.v and Laws.v are in the same directory called GroupTheory.

When I create a subdirectory called GroupTheory under GroupTheory, put all the compiled files there, and change

Require Import Laws.

to

Require Import GroupTheory.Laws.

then it works. But I don't think this manual work is necessary.

Maybe something is wrong with Makefile, so I looked into the Makefile and found following lines:

# This Makefile was generated by the command line :
# coq_makefile -f Make -o Makefile

And the content of the file 'Make' is as follows:

=============
-R . GroupTheory
./Group_definitions.v
./g2.v
./gr.v
./g3.v
./Z/Zle.v
./Z/Zbase.v
./Z/Nat_complements.v
./Z/Z_succ_pred.v
./Z/Zadd.v
./Laws.v
./Relations.v
./g1.v
=============

But I don't know how to change the file 'Make' or create right 'Makefile'.

Any help would be appreciated.

Gyesik