From 67f4332c9e802a0d272ac0670515d98d16cfebb4 Mon Sep 17 00:00:00 2001
From: Stefan Monnier
Date: Tue, 3 Jun 2014 02:51:24 +0000
Subject: Rename coq-smie-lexer.el to coq-smie.el.

---
 coq/ex/indent.v | 17 ++++++++++++-----
 1 file changed, 12 insertions(+), 5 deletions(-)

(limited to 'coq/ex')

diff --git a/coq/ex/indent.v b/coq/ex/indent.v
index c574f715..b524d956 100644
--- a/coq/ex/indent.v
+++ b/coq/ex/indent.v
@@ -9,12 +9,19 @@ Record a : Type := make_a {
                        aa : nat
                      }.
 
-Inductive test : nat -> Prop :=
-| C1 : forall n, test n
-| C2 : forall n, test n
-| C3 : forall n, test n
-| C4 : forall n, test n.
+{
+  Inductive test : nat -> Prop :=
+  | C1 : forall n, test n
+  | 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.
+}
 
 Lemma toto:nat.
 Proof.
-- 
cgit v1.2.3