From 18a802b2b35a4c16f6b38398a5276e29b5525f81 Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Wed, 19 Jun 2002 12:46:33 +0000
Subject: Add nested section example to increase the horror.

---
 etc/coq/nested.v | 20 +++++++++++++++++---
 1 file changed, 17 insertions(+), 3 deletions(-)

(limited to 'etc')

diff --git a/etc/coq/nested.v b/etc/coq/nested.v
index ab2af6c6..bd447157 100644
--- a/etc/coq/nested.v
+++ b/etc/coq/nested.v
@@ -2,7 +2,7 @@
 
     BUGS:
 
-      None???
+    - Nested sections...
 
 ======= Below here fixed
 
@@ -79,7 +79,21 @@ End Apple.
 Section Banana.
 
 Lemma Coq:  O=O. Auto. Save.   (* silly example to show that testing
-				  prompt to determine if we're in proof
-				  mode is not good enough. *)
+				  prompt in coq-proof-mode-p to determine 
+				  if we're in proof mode is not good enough. 
+				  Hopefully nobody calls their theorems "Coq".*)
 
 End Banana.
+
+(* Nested sections?  
+   Oh no, this is too horrible to even think about.  *)
+
+Section Cranberry.
+
+  Section Damson.
+   
+    Lemma CoqIsStrange:  O=O. Auto. Save.
+
+  End Damson.
+
+End Cranberry.
-- 
cgit v1.2.3