Fixing #183.

2 files changed, 18 insertions, 3 deletions

diff --git a/coq/coq-smie.el b/coq/coq-smie.el
index ce386c1f..33ef19d1 100644
--- a/coq/coq-smie.el
+++ b/coq/coq-smie.el
@@ -592,9 +592,13 @@ The point should be at the beginning of the command name."
 
      ;; FIXME: no token should end with "." except "." itself
      ; for "unfold in *|-*."
-     ((member tok '("*." "-*." "|-*." "*|-*.")) (forward-char 1) ".")
+     ((member tok '("*." "-*." "|-*." "*|-*."))
+      (forward-char (- (length tok) 1))
+      (coq-smie-.-deambiguate))
      ; for "unfold in *|-*;"
-     ((member tok '("*;" "-*;" "|-*;" "*|-*;")) (forward-char 1) "; tactic") ;; FIXME; can be "; ltac" too
+     ((member tok '("*;" "-*;" "|-*;" "*|-*;"))
+      ;; FIXME; can be "; ltac" too
+      (forward-char (- (length tok) 1)) "; tactic")
      ((and (string-match coq-bullet-regexp-nospace tok)
 	   (save-excursion (coq-empty-command-p)))
       (concat tok " bullet"))
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.