blob: 343fe85ac1cbc32b851c02c2e9dbe1fe402b1622 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
|
Here we have three projects a, b and c. The projects b and c are
totally independent from each other.
Strangely, project a contains a module Le, which clashes with
Coq.Arith.Le from the standard library.
Project b depends on a, more precisely, b/b.v requires a/Le.v.
File c/c.v require Le, but this refers to Coq.Arith.Le!!
Currently coqtop is not able to reset the LoadPath, therefore,
when first scripting b/b.v and then switching to c/c.v, coq
wrongly loads a/Le.vo! Vice versa, when first scripting c/c.v and
then switching to b/b.v, coq loads Coq.Arith.Le instead of
a/Le.vo!
Because coq-load-path is file-local, the dependency analysis
works correctly.
|
