I'm porting a Coq plugin from 8.11 to 8.12, and I understand that loadpaths now need to be qualified with a library name. Is there a difference between "Add Loadpath ... as Foo", "From Foo Require Import" vs "Add Rec Loadpath", "Require Import"
Also, what is the suggested way of making this change in the _CoqProject file, so I dont have to make the change in each file individually?
Thanks!
use -Q or -R in the coqproject
I did try using -R in the coqproject (I added a new line that says -R coq Foo, where coq is the folder where I want to import from). But I still need to change the imports to "From Foo Import ..." in each individual file, is that correct?
with -Q yes, with -R no
Last updated: Oct 13 2024 at 01:02 UTC