Add LoadPath in Coq 8.12.2


I have just upgraded my operating system, which has also involved
getting Coq 8.12.2 (December 2020)

Previously I was using Coq 8.11.2

The command
Add LoadPath "../tense-lns".
now seems to cause an error.

How do I change the command to get the same behaviour?

BTW, I've had a great deal of advice on the Coq-Club mailing list
about using a _CoqProject file, but it seems I can't do this without
stuffing up everyone who uses the same code - at any rate, early last
year, for several days, and over a dozen emails to the list, and lots
of advice from people then too, I tried to use a _CoqProject file
but it seemed either not possible or so difficult that it was
effectively impossible.

At any rate, my question now is about importing a compiled file,
say ../tense-lns/genT.vo, which (to quote an error message)
"contains library genT and not library xx.genT"

My code worked great using the Add LoadPath command above,
in Coq 8.11.2 (and earlier). So I just am asking how to do that now
(without being stuck using Coq 8.11 for ever)



You need to qualify your loadpath with a library name, the unqualified form has been removed, Add LoadPath "foo" as Foo.

You don’t absolutely have to use a _CoqProject file or coq_makefile if it doesn’t work for you (although this is surprising). But if you want to import compiled files, you do need to associate a logical name (e.g. Foo) to a directory. You should compile these files with the -R or -Q option of coqc to do so. Then you can use the command written by Emilio above, and you can import your files with From Foo Require Import ... (the From Foo is optional if you used the -R option).