diff options
| author |  Hendrik Tews <hendrik@askra.de> | 2011-05-20 06:38:04 +0000 |
|---|---|---|
| committer | Hendrik Tews <hendrik@askra.de> | 2011-05-20 06:38:04 +0000 |
| commit | d020f9c42ad658b05d669e10aef03f43e1605a98 (patch) | |
| tree | 2e54ba4a02808b6722fc8fc20c8cd7ec6d832a98 /coq/ex | |
| parent | 933e4ed71c8ef2e06addb473b8627efe9e196b46 (diff) | |
- minor changes: clean personal todo list + adjust test case description
Diffstat (limited to 'coq/ex')
| -rw-r--r-- | coq/ex/test-cases/change-ancestor/README | 7 |
1 files changed, 5 insertions, 2 deletions
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. |