From 6a2b111bc4ed9bcd8b4feb7fc83e93def431ee2c Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Wed, 12 Jun 2002 17:52:00 +0000
Subject: Add test t4 for extra depth of nesting

---
 etc/coq/nested.v | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

(limited to 'etc')

diff --git a/etc/coq/nested.v b/etc/coq/nested.v
index 21a874ac..975101cd 100644
--- a/etc/coq/nested.v
+++ b/etc/coq/nested.v
@@ -29,8 +29,10 @@ Case n. (* 5 "Undo" *)
 EAuto. (* 6 "Undo" *)
 
 Require Omega. (* 7 This needs "Back 1" to be retracted. *)
-Lemma t2 : O=O. Auto. Save. (* 8 "Back 1" or "Reset t2". *)
+  Lemma t2 : O=O. Auto. 
+    Lemma t4 : O=O. Auto. Save.
+  Save. (* 8 "Back 1" or "Reset t2". *)
 Intros. (* 9 "Undo" *)
-Lemma t3 : O=O. Auto. Save. (* 10 "Back 1" or "Reset t3" *)
+  Lemma t3 : O=O. Auto. Save. (* 10 "Back 1" or "Reset t3" *)
 EAuto. (* 11 "Undo" *)
 Save. (* 12 *)
-- 
cgit v1.2.3