From 05f9272860f9f57e6adfa150734ea7aa29702ca7 Mon Sep 17 00:00:00 2001
From: Hendrik Tews <hendrik@askra.de>
Date: Fri, 14 Jan 2011 15:50:47 +0000
Subject: - 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

---
 coq/ex/test-cases/README                             | 12 ++++++++++++
 .../retract-completely-asserted/.cvsignore           |  2 ++
 coq/ex/test-cases/retract-completely-asserted/README | 20 ++++++++++++++++++++
 coq/ex/test-cases/retract-completely-asserted/a.v    |  4 ++++
 coq/ex/test-cases/retract-completely-asserted/b.v    |  4 ++++
 coq/ex/test-cases/retract-completely-asserted/c.v    |  9 +++++++++
 6 files changed, 51 insertions(+)
 create mode 100644 coq/ex/test-cases/README
 create mode 100644 coq/ex/test-cases/retract-completely-asserted/.cvsignore
 create mode 100644 coq/ex/test-cases/retract-completely-asserted/README
 create mode 100644 coq/ex/test-cases/retract-completely-asserted/a.v
 create mode 100644 coq/ex/test-cases/retract-completely-asserted/b.v
 create mode 100644 coq/ex/test-cases/retract-completely-asserted/c.v

(limited to 'coq/ex')

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
-- 
cgit v1.2.3