From 2202c8a405f50dcb589f69db106afcdbdd22cafd Mon Sep 17 00:00:00 2001
From: Pierre Courtieu
Date: Tue, 23 May 2017 17:29:54 +0200
Subject: Fixing #183.

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

(limited to 'coq/ex')

diff --git a/coq/ex/indent.v b/coq/ex/indent.v
index 411347f0..1e9c17d8 100644
--- a/coq/ex/indent.v
+++ b/coq/ex/indent.v
@@ -91,6 +91,17 @@ Module Y.
     - induction x;simpl;intros...
     - induction x;simpl;intros...
   Qed.
+  Lemma L''' : forall x:nat , Nat.iter x (A:=nat) (plus 2) 0 >= x.
+  Proof using Type *.
+    intros x.
+    induction x;simpl;intros.  
+    admit.
+  Admitted.
+
+  Lemma L'''' : forall x:nat ,  0 <= x.
+  Proof (fun x : nat => Nat.le_0_l x).
+  (* no indentation here since the proof above closes the proof. *)
+  Definition foo:nat := 0.
 End Y.
 
 Function div2 (n : nat) {struct n}: nat :=
@@ -314,7 +325,7 @@ Module TC.
   
   Next Obligation.
   Proof.
-    unfold pointwise_relation, all in * .
+    unfold pointwise_relation, all in *.
     intro.
     intros y H.    
     intuition ; specialize (H x0) ; intuition.
-- 
cgit v1.2.3