Fixed an ineficiency in comment detection.

2 files changed, 102 insertions, 74 deletions

diff --git a/coq/coq-indent.el b/coq/coq-indent.el
index 8ee529ed..69951ab6 100644
--- a/coq/coq-indent.el
+++ b/coq/coq-indent.el
@@ -174,18 +174,19 @@ if found, to (point-max) otherwise. return true if found, nil otherwise."
 
 (defun coq-looking-at-comment ()
   "Return non-nil if point is inside a comment."
-  (save-excursion (coq-skip-until-one-comment-backward)))
+  (proof-inside-comment (+ 1 (point))))
 
 (defun coq-find-comment-start ()
   "Go to the current comment start.
 If inside nested comments, go to the start of the
 outer most comment. Return the position of the comment start. If not inside a
 comment, return nil and does not move the point."
-  (let ((prevpos (point)) (init (point)))
-    (while (coq-skip-until-one-comment-backward)
-      (setq prevpos (point)))
-    (goto-char prevpos)
-    (if (= prevpos init) nil prevpos)))
+  (when (coq-looking-at-comment)
+    (let ((prevpos (point)) (init (point)))
+      (while (coq-skip-until-one-comment-backward)
+        (setq prevpos (point)))
+      (goto-char prevpos)
+      (if (= prevpos init) nil prevpos))))
 
 (defun coq-find-comment-end ()
   "Go to the current comment end.
diff --git a/coq/ex/indent.v b/coq/ex/indent.v
index 3e1b60ed..752bc4f9 100644
--- a/coq/ex/indent.v
+++ b/coq/ex/indent.v
@@ -6,13 +6,13 @@ Notation "[ a ; .. ; b ]" := (a :: .. (b :: []) ..) : list_scope.
 Require Import Arith.
 
 Record a : Type := make_a {
-  aa : nat
-}.
+                       aa : nat
+                     }.
 
 Lemma toto:nat.
 Proof.
   {{
-    exact 3.
+     exact 3.
   }}
 Qed.
 
@@ -34,37 +34,37 @@ Function div2 (n : nat) {struct n}: nat :=
 Module M1.
   Module M2.
     Lemma l1: forall n:nat, n = n. 
-      auto.
+    auto.
     Qed.
     Lemma l2: forall n:nat, n = n. 
-      auto. Qed.
+    auto. Qed.
     Lemma l3: forall n:nat, n <= n. auto. Qed.
     (*   Lemma l4: forall n:nat, n <= n. Proof. intro. Qed. *)
     Lemma l5 : forall n:nat, n <= n.
     Proof. auto.
     Qed.
     Lemma l6: forall n:nat, n = n. 
-      intros.
-      Lemma l7: forall n:nat, n = n. 
-        destruct n.
-        BeginSubproof.
-          auto.
-        EndSubproof.
-        BeginSubproof.
-          destruct n.
-          BeginSubproof.
-            auto.
-          EndSubproof.
-          auto.
-        EndSubproof.        
-      Qed.
+    intros.
+    Lemma l7: forall n:nat, n = n. 
+    destruct n.
+    BeginSubproof.
+      auto.
+    EndSubproof.
+    BeginSubproof.
+      destruct n.
       BeginSubproof.
-        destruct n.
-        BeginSubproof.
-          auto. EndSubproof.
-        BeginSubproof. auto.
-        EndSubproof.
+        auto.
+      EndSubproof.
+      auto.
+    EndSubproof.        
+    Qed.
+    BeginSubproof.
+      destruct n.
+      BeginSubproof.
+        auto. EndSubproof.
+      BeginSubproof. auto.
       EndSubproof.
+    EndSubproof.
     Qed.
   End M2.
 End M1.
@@ -73,8 +73,10 @@ End M1.
 Module M1'.
   Module M2'.
     Lemma l6: forall n:nat, n = n. 
+    Proof.
       intros.
       Lemma l7: forall n:nat, n = n. 
+      Proof.
         destruct n.
         {
           auto.
@@ -83,8 +85,8 @@ Module M1'.
           destruct n.
           {
             idtac;[
-              auto
-            ].
+                     auto
+                   ].
           }
           auto.
         } 
@@ -99,46 +101,70 @@ Module M1'.
 End M1'.
 
 
+Module M4'.
+  Module M2'.
+    Lemma l6: forall n:nat, n = n. 
+    Proof.
+      intros.
+      Lemma l7: forall n:nat, n = n. 
+      Proof.
+        destruct n.
+        - auto.
+        - destruct n.
+          + idtac;[
+              auto
+            ].
+          + auto.
+      Qed.
+      {destruct n.
+        - auto.
+        - auto. 
+      }
+    Qed.
+  End M2'.
+End M1'.
+
+
 Module M1''.
   Module M2''.
     Lemma l7: forall n:nat, n = n. 
-      destruct n.
-      { auto. }
-      { destruct n.
-        { idtac; [ auto ]. }
-        auto. } 
+    destruct n.
+    { auto. }
+    { destruct n.
+      { idtac; [ auto ]. }
+      auto. } 
     Qed.
   End M2''.
 End M1''.
 
 
 Record rec:Set := { 
-  fld1:nat;
-  fld2:nat;
-  fld3:bool
-}.
+                 fld1:nat;
+                 fld2:nat;
+                 fld3:bool
+               }.
 
 Class cla {X:Set}:Set := { 
-  cfld1:nat;
-  cld2:nat;
-  cld3:bool
-}.
+                        cfld1:nat;
+                        cld2:nat;
+                        cld3:bool
+                      }.
 
 
 
 Module X.
   Lemma l :
     forall r:rec,
-      exists r':rec,
-        r'.(fld1) = r.(fld2)/\ r'.(fld2) = r.(fld1).
+    exists r':rec,
+      r'.(fld1) = r.(fld2)/\ r'.(fld2) = r.(fld1).
   Proof.
     intros r.  
     { exists 
-      {|
-        fld1:=r.(fld2);
-        fld2:=r.(fld1);
-        fld3:=false
-      |}.
+        {|
+          fld1:=r.(fld2);
+          fld2:=r.(fld1);
+          fld3:=false
+        |}.
       split.
       {auto. }
       {auto. }
@@ -148,23 +174,24 @@ Module X.
 
   Lemma l2 :
     forall r:rec,
-      exists r':rec,r'.(fld1) = r.(fld2) /\ r'.(fld2) = r.(fld1).
+    exists r':rec,r'.(fld1) = r.(fld2) /\ r'.(fld2) = r.(fld1).
+  Proof.
     intros r.  
     {{
-        idtac;
-          exists 
-            {|
-              fld1:=r.(fld2);
-              fld2:=r.(fld1);
-              fld3:=false
-            |}.
-    (* ltac *)
-        match goal with
-          | _:rec |- ?a /\ ?b => split
-          | _ => fail    
-        end.
-        {auto. }
-        {auto. }}}
+       idtac;
+         exists 
+           {|
+             fld1:=r.(fld2);
+             fld2:=r.(fld1);
+             fld3:=false
+           |}.
+       (* ltac *)
+       match goal with
+         | _:rec |- ?a /\ ?b => split
+         | _ => fail    
+       end.
+       {auto. }
+       {auto. }}}
   Qed.
 End X.
 
@@ -196,11 +223,11 @@ Module foo.
     Proper (pointwise_relation A iff ==> iff) (@all A).
 
   Next Obligation.
-  Proof.
-    unfold pointwise_relation, all in * .
-    intro.
-    intros y H.    
-    intuition ; specialize (H x0) ; intuition.
-  Qed.
-  
+    Proof.
+      unfold pointwise_relation, all in * .
+      intro.
+      intros y H.    
+      intuition ; specialize (H x0) ; intuition.
+    Qed.
+    
 End foo.