diff options
Diffstat (limited to 'coq/ex/test-cases/stale-load-path/README')
| -rw-r--r-- | coq/ex/test-cases/stale-load-path/README | 18 |
1 files changed, 18 insertions, 0 deletions
diff --git a/coq/ex/test-cases/stale-load-path/README b/coq/ex/test-cases/stale-load-path/README new file mode 100644 index 00000000..343fe85a --- /dev/null +++ b/coq/ex/test-cases/stale-load-path/README @@ -0,0 +1,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. |