From d020f9c42ad658b05d669e10aef03f43e1605a98 Mon Sep 17 00:00:00 2001 From: Hendrik Tews Date: Fri, 20 May 2011 06:38:04 +0000 Subject: - minor changes: clean personal todo list + adjust test case description --- coq/ex/test-cases/change-ancestor/README | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) (limited to 'coq/ex') diff --git a/coq/ex/test-cases/change-ancestor/README b/coq/ex/test-cases/change-ancestor/README index 056bd892..91dc814d 100644 --- a/coq/ex/test-cases/change-ancestor/README +++ b/coq/ex/test-cases/change-ancestor/README @@ -16,8 +16,11 @@ To reproduce the test do the following: This test case triggers a bug in the cvs version from -2011-05-12 12:10:00 UTC. The bug is that after unlocking the -ancestor a.v only the newly added text is sent to Coq. Therefore +2011-05-12 12:10:00 UTC. The bug has been fixed, see issue +http://proofgeneral.inf.ed.ac.uk/trac/ticket/400 . + +The bug is that after unlocking the +ancestor a.v, only the newly added text is sent to Coq. Therefore Coq responds with an error (reference a was not found in the current environment). When one asserts a.v from the beginning, the definition of b is of course accepted. -- cgit v1.2.3