From aa76421458123fc17a61f4b7218a175ece5e9404 Mon Sep 17 00:00:00 2001 From: Hendrik Tews Date: Mon, 17 Jan 2011 07:44:42 +0000 Subject: fix problems in test cases coq/ex/test-cases/multiple-files-single-dir and multiple-files-multiple-dir --- coq/ex/test-cases/README | 2 -- coq/ex/test-cases/multiple-files-multiple-dir/README | 5 ----- coq/ex/test-cases/multiple-files-single-dir/.cvsignore | 2 ++ coq/ex/test-cases/multiple-files-single-dir/README | 4 ++++ 4 files changed, 6 insertions(+), 7 deletions(-) create mode 100644 coq/ex/test-cases/multiple-files-single-dir/.cvsignore (limited to 'coq/ex') 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! + -- cgit v1.2.3