Add nested section example to increase the horror.

1 files changed, 17 insertions, 3 deletions

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.