diff options
| author | Hendrik Tews | 2011-01-14 15:50:47 +0000 |
|---|---|---|
| committer | Hendrik Tews | 2011-01-14 15:50:47 +0000 |
| commit | 05f9272860f9f57e6adfa150734ea7aa29702ca7 (patch) | |
| tree | 2f26bec12453529d2e89efa31dcbf2ae75b2302c /coq/ex/test-cases/README | |
| parent | a2ba24cc1172258abd98eee6350cdb672e50e4de (diff) | |
- move proof-no-fully-processed-buffer to generic/proof-config
- add documentation for it
- add a test case demonstrating it in
coq/ex/test-cases/retract-completely-asserted
Diffstat (limited to 'coq/ex/test-cases/README')
| -rw-r--r-- | coq/ex/test-cases/README | 12 |
1 files changed, 12 insertions, 0 deletions
diff --git a/coq/ex/test-cases/README b/coq/ex/test-cases/README new file mode 100644 index 00000000..62081521 --- /dev/null +++ b/coq/ex/test-cases/README @@ -0,0 +1,12 @@ +This directory contains test cases for coq ProofGeneral, +especially for its multi-file support. + +Each test case is in one subdirectory. Each such subdirectory has +a README file, describing the test case. + + +Overview of the test cases: + +retract-completely-asserted + test how proof-no-fully-processed-buffer retracts fully + asserted buffers |