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
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
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)