From 1a0edf9dc05b8065e1ce9f7c6b6f9ea0b63c7088 Mon Sep 17 00:00:00 2001
From: Pierre Courtieu
Date: Wed, 8 Jun 2011 22:49:47 +0000
Subject: Added one indentation example.

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

diff --git a/coq/ex/indent.v b/coq/ex/indent.v
index ce8e1edb..c9583b3e 100644
--- a/coq/ex/indent.v
+++ b/coq/ex/indent.v
@@ -1,5 +1,10 @@
 Require Import Arith.
 
+Lemma L : forall x:nat , nat_iter x (A:=nat) (plus 2) 0 >= x.
+Proof.
+  intros x;
+    toto.
+Qed.
 
 Function div2 (n : nat) {struct n}: nat :=
   match n with
-- 
cgit v1.2.3