diff options
Diffstat (limited to 'coq/ex')
-rw-r--r-- | coq/ex/test-cases/README | 12 | ||||
-rw-r--r-- | coq/ex/test-cases/retract-completely-asserted/.cvsignore | 2 | ||||
-rw-r--r-- | coq/ex/test-cases/retract-completely-asserted/README | 20 | ||||
-rw-r--r-- | coq/ex/test-cases/retract-completely-asserted/a.v | 4 | ||||
-rw-r--r-- | coq/ex/test-cases/retract-completely-asserted/b.v | 4 | ||||
-rw-r--r-- | coq/ex/test-cases/retract-completely-asserted/c.v | 9 |
6 files changed, 51 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 diff --git a/coq/ex/test-cases/retract-completely-asserted/.cvsignore b/coq/ex/test-cases/retract-completely-asserted/.cvsignore new file mode 100644 index 00000000..480bc6d5 --- /dev/null +++ b/coq/ex/test-cases/retract-completely-asserted/.cvsignore @@ -0,0 +1,2 @@ +*.vo +*.glob diff --git a/coq/ex/test-cases/retract-completely-asserted/README b/coq/ex/test-cases/retract-completely-asserted/README new file mode 100644 index 00000000..68cca029 --- /dev/null +++ b/coq/ex/test-cases/retract-completely-asserted/README @@ -0,0 +1,20 @@ +In coq different modules may contain definition with the same +name, because for coq they have different "absolute names" because +they are in different modules. + +To provoke an error inside ProofGeneral on correct coq input, +do the following: +- Visit a.v and script the initial comment. +- Set proof-no-fully-processed-buffer to nil. +- assert buffer a.v completely +- switch to b.v +- scripting "Definition a" in b.v will give the error "a already + exists" + +Now retract a.v, set proof-no-fully-processed-buffer to t and try +again. + +To see that the example is indeed valid, script c.v. (For c.v you +either have to switch coq-recompile-before-require to t or you +have to compile modules a and b yourself with "coqc a" and "coqc b".) + diff --git a/coq/ex/test-cases/retract-completely-asserted/a.v b/coq/ex/test-cases/retract-completely-asserted/a.v new file mode 100644 index 00000000..ea9a099d --- /dev/null +++ b/coq/ex/test-cases/retract-completely-asserted/a.v @@ -0,0 +1,4 @@ + +(* The following defines the absolut name a.a *) + +Definition a := 0.
\ No newline at end of file diff --git a/coq/ex/test-cases/retract-completely-asserted/b.v b/coq/ex/test-cases/retract-completely-asserted/b.v new file mode 100644 index 00000000..d07522ba --- /dev/null +++ b/coq/ex/test-cases/retract-completely-asserted/b.v @@ -0,0 +1,4 @@ + +(* The following defines the absolute name b.a *) + +Definition a := 1.
\ No newline at end of file diff --git a/coq/ex/test-cases/retract-completely-asserted/c.v b/coq/ex/test-cases/retract-completely-asserted/c.v new file mode 100644 index 00000000..bd82b351 --- /dev/null +++ b/coq/ex/test-cases/retract-completely-asserted/c.v @@ -0,0 +1,9 @@ + +Require Import a. +Require Import b. + +(* b.a hides a.a, therefore the partial name "a" refers to b.a *) +Print a. + +(* a.a is available under its longer name *) +Print a.a.
\ No newline at end of file |