From 7238c3d7555b01d814666e12ec24e87a1ed154c5 Mon Sep 17 00:00:00 2001
From: Pierre Courtieu <courtieu@lri.fr>
Date: Fri, 8 Jul 2011 13:08:04 +0000
Subject: Fixing the scripting of new subproof script parenthesizing ({ and }).

---
 coq/ex/indent.v | 27 +++++++++++++++++++++------
 1 file changed, 21 insertions(+), 6 deletions(-)

(limited to 'coq/ex')

diff --git a/coq/ex/indent.v b/coq/ex/indent.v
index f2ba0f9d..3e1b60ed 100644
--- a/coq/ex/indent.v
+++ b/coq/ex/indent.v
@@ -16,11 +16,12 @@ Proof.
   }}
 Qed.
 
-
-Lemma L : forall x:nat , nat_iter x (A:=nat) (plus 2) 0 >= x.
-Proof.
-  induction x;simpl;intros;auto with arith.
-Qed.
+Module Y.
+  Lemma L : forall x:nat , nat_iter x (A:=nat) (plus 2) 0 >= x.
+  Proof with auto with arith.
+    induction x;simpl;intros...
+  Qed.
+End Y.
 
 Function div2 (n : nat) {struct n}: nat :=
   match n with
@@ -86,7 +87,7 @@ Module M1'.
             ].
           }
           auto.
-        }        
+        } 
       Qed.
       {destruct n.
         {
@@ -97,6 +98,20 @@ Module M1'.
   End M2'.
 End M1'.
 
+
+Module M1''.
+  Module M2''.
+    Lemma l7: forall n:nat, n = n. 
+      destruct n.
+      { auto. }
+      { destruct n.
+        { idtac; [ auto ]. }
+        auto. } 
+    Qed.
+  End M2''.
+End M1''.
+
+
 Record rec:Set := { 
   fld1:nat;
   fld2:nat;
-- 
cgit v1.2.3