aboutsummaryrefslogtreecommitdiffhomepage
path: root/coq/ex/test-cases/add-load-path-unsupported/README
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!