blob: 273368cdda84d4b475e30577ab9a6db48e939ae7 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
|
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!!
The resulting LoadPath confusion bug, which is described in the
following, has been fixed with the commit
around 2011-01-18 21:45:00 UTC.
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.
|
