bbv/theories checkin breaks all projects using bbv

[vmurali]

Looks like I didn't realize this affects all the projects using bbv :(

In my setup, my _CoqProject using bbv has the following:

-R . Kami
-R ../bbv bbv

And inside my files (in Kami), I do "Require Import bbv/Word.".

The following change to _CoqProject does not work.
-R . Kami
-R ../bbv/theories bbv

Also, why is this a good idea as opposed to storing the .vo files directly in the directories named after the project?

[samuelgruetter]

I'm surprised that this change doesn't work for you, because for bedrock2, it worked: mit-plv/bedrock2@0d1e6eb
And for riscv-coq too: mit-plv/riscv-coq@913b989
I really just had to insert /theories in the right place.
Are you sure that's not just a "should have started from a fresh clone"?

[vmurali]

I had changed only _CoqProject, not the Makefile. It works if I change the Makefile also. We need automate this process of setting the flags in the Makefile, since it is already there in the _CoqProject!