diff options
| author |  Hendrik Tews <hendrik@askra.de> | 2011-01-18 21:46:18 +0000 |
|---|---|---|
| committer | Hendrik Tews <hendrik@askra.de> | 2011-01-18 21:46:18 +0000 |
| commit | 358b338316430fe8707780985702b2a925a45abc (patch) | |
| tree | 0c058e30fb1c42a714a40731aa442c99f9007c0d /coq/ex | |
| parent | 680d718e1e3ca280dfc35fc3f1807d0c373a1870 (diff) | |
- fixed stale load path problem with killing the proof shell in
the deactivation-hook
Diffstat (limited to 'coq/ex')
| -rw-r--r-- | coq/ex/test-cases/README | 1 | ||||
| -rw-r--r-- | coq/ex/test-cases/stale-load-path/README | 4 | ||||
| -rw-r--r-- | coq/ex/test-cases/stale-load-path/a/.cvsignore | 2 |
3 files changed, 6 insertions, 1 deletions
diff --git a/coq/ex/test-cases/README b/coq/ex/test-cases/README index 7d91b29f..b89cc230 100644 --- a/coq/ex/test-cases/README +++ b/coq/ex/test-cases/README @@ -26,4 +26,3 @@ retract-completely-asserted stale-load-path test switching between files with different load path. - (triggers known bugs) diff --git a/coq/ex/test-cases/stale-load-path/README b/coq/ex/test-cases/stale-load-path/README index 343fe85a..273368cd 100644 --- a/coq/ex/test-cases/stale-load-path/README +++ b/coq/ex/test-cases/stale-load-path/README @@ -8,6 +8,10 @@ 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 diff --git a/coq/ex/test-cases/stale-load-path/a/.cvsignore b/coq/ex/test-cases/stale-load-path/a/.cvsignore new file mode 100644 index 00000000..e940bcb4 --- /dev/null +++ b/coq/ex/test-cases/stale-load-path/a/.cvsignore @@ -0,0 +1,2 @@ +*.glob +*.vo |