From a9660f46b64132dec0d0efc8ff4419ec8899558b Mon Sep 17 00:00:00 2001
From: Pierre Courtieu
Date: Wed, 24 Dec 2014 14:13:23 +0000
Subject: fixed a bug in command parsing for coq, due to recent changes.

---
 coq/ex/indent.v | 14 +++++++-------
 1 file changed, 7 insertions(+), 7 deletions(-)

(limited to 'coq/ex')

diff --git a/coq/ex/indent.v b/coq/ex/indent.v
index 7218fa63..6644df83 100644
--- a/coq/ex/indent.v
+++ b/coq/ex/indent.v
@@ -15,22 +15,22 @@ Record a : Type := make_a {
   | C2 : forall n, test n
   | C3 : forall n, test n
   | C4 : forall n, test n.
-
+  
   Inductive test2 : nat -> Prop
     := C1 : forall n, test n
      | C2 : forall n, test n
      | C3 : forall n, test n
      | C4 : forall n, test n.
-
+  
   Let x : = 1.  Let y := 2.
-                
+  
   Let y := (1, 2, 3,
             4, 5).
   
-    Inductive test3             (* fixindent *)
-      : nat -> Prop
-      := C1 : forall n, test n
-       | C2 : forall n, test n
+  Inductive test3             (* fixindent *)
+    : nat -> Prop
+    := C1 : forall n, test n
+     | C2 : forall n, test n
 }
 
 Lemma toto:nat.
-- 
cgit v1.2.3