The Coq mailing list

[Enrico Tassi <enrico.tassi AT inria.fr>]

It should look like

-R . MyProject

File1.v

...

FileN.v

And you should then invoke 

coq_makefile -f _CoqProject -o Makefile 

And finally

make

See also https://coq.inria.fr/distrib/current/refman/practical-tools/utilities.html#building-a-coq-project-with-coq-makefile

On Sep 24, 2020 07:50, Patricia Peratto <psperatto AT vera.com.uy> wrote:

I want to compile a simple file called Ident.v.

I have written the following _CoqProject in

the same folder where I have the Ident.v file.

-R . .
-arg ./Ident.v

when I try to load the file from which I import

Ident.v gives a compilation error message.

I don't know how to write the _CoqProject file.

Can you help me?

Regards,

Patricia