blob: d6e56c259134c3e500b9eb8f7e8c4f892e644e4d (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
|
b/b.v depends on a/a.v and the code is correct because of Add
LoadPath in b.
Scripting b/b.v works if coq-recompile-before-require is set to
nil and if a/a.v is compiled manually.
This problem is not considered a bug, but a feature that does not
make much sense to implement, because apparently nobody is using
Add LoadPath.
Note that not even coqdep is able to handle b/b.v correctly!
|
