- 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

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