diff options
| author |  Hendrik Tews <hendrik@askra.de> | 2011-01-17 07:44:42 +0000 |
|---|---|---|
| committer | Hendrik Tews <hendrik@askra.de> | 2011-01-17 07:44:42 +0000 |
| commit | aa76421458123fc17a61f4b7218a175ece5e9404 (patch) | |
| tree | 0245b800d05734b15e2d65be0c5dd9005c143036 /coq/ex | |
| parent | a8855cbf77923217c40bc7abe289f778392b25a9 (diff) | |
fix problems in test cases
coq/ex/test-cases/multiple-files-single-dir and multiple-files-multiple-dir
Diffstat (limited to 'coq/ex')
| -rw-r--r-- | coq/ex/test-cases/README | 2 | ||||
| -rw-r--r-- | coq/ex/test-cases/multiple-files-multiple-dir/README | 5 | ||||
| -rw-r--r-- | coq/ex/test-cases/multiple-files-single-dir/.cvsignore | 2 | ||||
| -rw-r--r-- | coq/ex/test-cases/multiple-files-single-dir/README | 4 |
4 files changed, 6 insertions, 7 deletions
diff --git a/coq/ex/test-cases/README b/coq/ex/test-cases/README index 3943793a..7d91b29f 100644 --- a/coq/ex/test-cases/README +++ b/coq/ex/test-cases/README @@ -12,11 +12,9 @@ add-load-path-unsupported multiple-files-multiple-dir working with multiple files in a multiple directories - (triggers known bugs) multiple-files-single-dir working with multiple files in a single directory - (triggers known bugs) require-string test Require "x.vo" diff --git a/coq/ex/test-cases/multiple-files-multiple-dir/README b/coq/ex/test-cases/multiple-files-multiple-dir/README index 82c7fc2a..3e8500ff 100644 --- a/coq/ex/test-cases/multiple-files-multiple-dir/README +++ b/coq/ex/test-cases/multiple-files-multiple-dir/README @@ -16,8 +16,3 @@ a. Script c.v and watch the compilation messages in *Messages*. Touch any file and retract and assert the Require in c. - -The bugs described in ../multiple-files-single-dir/README can -also be reproduced here. - - diff --git a/coq/ex/test-cases/multiple-files-single-dir/.cvsignore b/coq/ex/test-cases/multiple-files-single-dir/.cvsignore new file mode 100644 index 00000000..e940bcb4 --- /dev/null +++ b/coq/ex/test-cases/multiple-files-single-dir/.cvsignore @@ -0,0 +1,2 @@ +*.glob +*.vo diff --git a/coq/ex/test-cases/multiple-files-single-dir/README b/coq/ex/test-cases/multiple-files-single-dir/README index db1a6a9b..60649b07 100644 --- a/coq/ex/test-cases/multiple-files-single-dir/README +++ b/coq/ex/test-cases/multiple-files-single-dir/README @@ -23,6 +23,9 @@ Some tests: simply do touch), retract the Require in f.v, and watch the compilation messages when you assert it again. +The following two problems have been fixed with the commit around +2011-01-17 07:45:00 UTC. + The implementation in Proof General cvs at 2011-01-14 20:03:51 UTC has an embarrassing bug: Touching b.v causes recompilation of b.v and d.v but not of e.v! @@ -30,3 +33,4 @@ and d.v but not of e.v! Another problem is the following: After a consistent compilation, change b.v and recompile it outside of Proof General. Then script f.v -- Proof General will not recompile d and e! + |