From ea043143aa90e0013bb8c4bd2ceb59217618f598 Mon Sep 17 00:00:00 2001
From: Pierre Courtieu <courtieu@lri.fr>
Date: Thu, 9 Sep 2010 11:27:49 +0000
Subject: Fixed small bugs in indentation.

---
 coq/ex/indent.v | 30 ++++++++++++++++++++++++++++++
 1 file changed, 30 insertions(+)
 create mode 100644 coq/ex/indent.v

(limited to 'coq/ex')

diff --git a/coq/ex/indent.v b/coq/ex/indent.v
new file mode 100644
index 00000000..b06ae922
--- /dev/null
+++ b/coq/ex/indent.v
@@ -0,0 +1,30 @@
+Require Import Arith.
+
+
+Function div2 (n : nat) {struct n}: nat :=
+  match n with
+    | 0 => 0
+    | 1 => 0
+    | S (S n') => S (div2 n')
+  end.
+
+
+Module toto.
+  Lemma l1: forall n:nat, n = n. 
+    toto.
+  Qed.
+  Lemma l2: forall n:nat, n = n. 
+  toto. Qed.
+  Lemma l3: forall n:nat, n <= n. intro. Qed.
+  Lemma l4: forall n:nat, n <= n. Proof. intro. Qed.
+  Lemma l5 : forall n:nat, n <= n.
+  Proof. intro.
+  Qed.
+  Lemma l6: forall n:nat, n = n. 
+    toto.
+    Lemma l7: forall n:nat, n = n. 
+      toto.
+    Qed.
+  Qed.
+End toto.
+
-- 
cgit v1.2.3