There's this library I'd like to use. The idea is to be able to use this library with
Require Import easily in any other
In the readme of said library, it recommends to include the library in my developments. So I understand I should add to the _CoqProject of this library (and not of any other new project which will use this library) the path to the directory that contains the _CoqProject file of this library.
coq_makefile -f _CoqProject -o Makefile
as is recommended in this stackoverflow answer.
However, when I
make, I get the following error.
I just downloaded the library and put it in some random directory to do this. Should it be somewhere in particular instead?
Sadly the coq.inria webpage seems to be down for the time being so I can't check the official documentation on
_CoqProject for which I know almost nothing about.
Thanks in advance for any help!