Fixes and cleanups for coq-indent-line, see Trac #172

1 files changed, 239 insertions, 229 deletions

diff --git a/coq/coq-indent.el b/coq/coq-indent.el
index 5f8b3f72..32979dee 100644
--- a/coq/coq-indent.el
+++ b/coq/coq-indent.el
@@ -1,29 +1,36 @@
+;;; coq-indent.el ---
 ; coq-syntax.el indentation stuff for Coq
-;; Copyright (C) 1997, 1998 LFCS Edinburgh. 
+;; Copyright (C) 1997, 1998 LFCS Edinburgh.
 ;; Authors: Pierre Courtieu
 ;; Maintainer: Pierre Courtieu <courtieu@lri.fr>
 
 ;;Pierre: This is experimental, the code is rather ugly for the moment.
 
 
+
+;;; Commentary:
+;; 
+
 (require 'coq-syntax)
 
+;;; Code:
 (defconst coq-any-command-regexp
   (proof-regexp-alt (proof-ids-to-regexp coq-keywords)))
 
 (defconst coq-indent-inner-regexp
-  (proof-regexp-alt 
-   "[[]()]" "|" "šÕ" ;; forall with x-symbol (nomule) must not be enclosed by \\<and
-                                        ;\\> . "~" forall x-symb mule but interacts
-                                        ;with 'not'
-   (proof-ids-to-regexp   
+  (proof-regexp-alt
+   "[[]()]" "|" "šÕ"
+   ;; forall with x-symbol (nomule) must not be enclosed by \\<and
+   ;;\\> . "~" forall x-symb mule but interacts
+   ;;with 'not'
+   (proof-ids-to-regexp
     '("as" "Cases" "match" "else" "Fix" "forall" "fun" "if" "into" "let" "then"
       "using" "after"))))
 ; "ALL" "True" "False" "EX" "end" "in" "of" "with"
 
 (defconst coq-comment-start-regexp "(\\*")
 (defconst coq-comment-end-regexp "\\*)")
-(defconst coq-comment-start-or-end-regexp 
+(defconst coq-comment-start-or-end-regexp
   (concat coq-comment-start-regexp "\\|" coq-comment-end-regexp))
 (defconst coq-indent-open-regexp
   (proof-regexp-alt ;(proof-ids-to-regexp coq-keywords-goal) goal-command-p instead
@@ -31,8 +38,8 @@
    "\\s("))
 
 (defconst coq-indent-close-regexp
-  (proof-regexp-alt (proof-ids-to-regexp coq-keywords-save) 
-                    (proof-ids-to-regexp '("end" "End")) 
+  (proof-regexp-alt (proof-ids-to-regexp coq-keywords-save)
+                    (proof-ids-to-regexp '("end" "End"))
                     "\\s)"))
 
 (defconst coq-indent-closepar-regexp "\\s)")
@@ -44,7 +51,7 @@
                     coq-indent-inner-regexp coq-any-command-regexp
                     (proof-ids-to-regexp coq-tacticals)
                     (proof-ids-to-regexp coq-tactics)))
-(defconst coq-indent-kw 
+(defconst coq-indent-kw
   (proof-regexp-alt coq-any-command-regexp coq-indent-inner-regexp
                     (proof-ids-to-regexp coq-tacticals)
                     (proof-ids-to-regexp coq-tactics)))
@@ -59,7 +66,8 @@
 ;;;; End of regexps
 
 (defun coq-indent-goal-command-p (str)
-  "Syntactical detection of a coq goal opening.  Only used in indentation code and in
+  "Syntactical detection of a coq goal opening.
+Only used in indentation code and in
 v8.0 compatibility mode.  Module, Definition and Function need a special parsing to
 detect if they start something or not."
   (let* ((match (coq-count-match "\\<match\\>" str))
@@ -68,40 +76,42 @@ detect if they start something or not."
          (affect (coq-count-match ":=" str)))
 		  
     (and (proof-string-match coq-goal-command-regexp str)
-         (not 
+         (not
           (and (proof-string-match "\\`\\(Local\\|Definition\\|Lemma\\|Module\\)\\>" str)
                (not (= letwith affect))))
          (not (proof-string-match "\\`Declare\\s-+Module\\(\\w\\|\\s-\\|<\\)*:" str))
-         (not 
+         (not
           (and (proof-string-match "\\`\\(Function\\|GenFixpoint\\)\\>" str)
                (not (proof-string-match "{\\s-*\\(wf\\|measure\\)" str))))
          )))
 
 ;; ". " and "... " are command endings, ".. " is not, same as in
 ;; proof-script-command-end-regexp in coq.el
-(defconst coq-end-command-regexp 
+(defconst coq-end-command-regexp
   "\\(?:[^.]\\|\\.\\.\\)\\(\\.\\)\\(?:\\s-\\|\\'\\)")
 ;  "\\(?:[^.]\\|\\(?:\\.\\.\\)\\)\\(\\.\\)\\(?:\\s-\\|\\'\\)")
 
 
 (defun coq-search-comment-delimiter-forward ()
-  "Search forward for a comment start (return 1) or end (return -1).  Return
-nil if not found."
+  "Search forward for a comment start (return 1) or end (return -1).
+Return nil if not found."
   (when (re-search-forward coq-comment-start-or-end-regexp nil 'dummy)
-    (save-excursion 
+    (save-excursion
       (goto-char (match-beginning 0))
       (if (looking-at coq-comment-start-regexp) 1 -1))))
 
 
 (defun coq-search-comment-delimiter-backward ()
-  "Search backward for a comment start (return 1) or end (return -1). Return
-nil if not found."
+  "Search backward for a comment start (return 1) or end (return -1).
+Return nil if not found."
   (when (re-search-backward coq-comment-start-or-end-regexp nil 'dummy)
       (if (looking-at coq-comment-start-regexp) 1 -1)))
 
 
 (defun coq-skip-until-one-comment-backward ()
-  "Skips comments and normal text until finding an unclosed comment start. Return nil if not found. Point is moved to the the unclosed comment start if found, to (point-max) otherwise."
+  "Skips comments and normal text until finding an unclosed comment start.
+Return nil if not found.  Point is moved to the the unclosed comment start
+if found, to (point-max) otherwise."
   (ignore-errors (backward-char 1))       ; if point is between '(' and '*'
   (if (looking-at coq-comment-start-regexp) t
     (forward-char 1)
@@ -128,7 +138,8 @@ nil if not found."
   (save-excursion (coq-skip-until-one-comment-backward)))
 
 (defun coq-find-comment-start ()
-  "Go to the current comment start. If inside nested comments, go to the start of the
+  "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)))
@@ -138,7 +149,8 @@ comment, return nil and does not move the point."
     (if (= prevpos init) nil prevpos)))
 
 (defun coq-find-comment-end ()
-  "Go to the current comment end. If inside nested comments, go to the end of the
+  "Go to the current comment end.
+If inside nested comments, go to the end of the
 outer most comment. Return the position of the end of comment end. If not inside a
 comment, return nil and does not move the point."
   (let ((prevpos (point)) (init (point)))
@@ -150,8 +162,8 @@ comment, return nil and does not move the point."
 ; generic function is wrong when the point in between ( and *
 ; moreover xemacs does not deal with nested comments
 (defun coq-looking-at-syntactic-context ()
-  "See `proof-looking-at-syntactic-context'. Use this one for coq instead of the
-generic one."
+  "See `proof-looking-at-syntactic-context'.
+Use this one for coq instead of the generic one."
   (if (coq-looking-at-comment) 'comment
     (proof-looking-at-syntactic-context)))
 
@@ -163,12 +175,13 @@ generic one."
 
 
 (defun coq-find-not-in-comment-backward (reg &optional lim submatch)
-  "Moves to the first not commented occurrence of REG found looking up.  The point is
+  "Moves to the first not commented occurrence of REG found looking up.
+The point is
 put exactly before the occurrence if SUBMATCH is nil, otherwise the point is put
 before SUBMATCHnth matched sub-expression (see `match-string').  If no occurrence is
 found, go as far as possible and return nil."
   (coq-find-comment-start) ; first go out of comment if inside some
-  (let ((found nil) (continue t) 
+  (let ((found nil) (continue t)
         (regexp (concat coq-comment-end-regexp "\\|" reg)))
     (while (and (not found) continue)
       (setq continue (re-search-backward regexp lim 'dummy))
@@ -182,12 +195,13 @@ found, go as far as possible and return nil."
 
 
 (defun coq-find-not-in-comment-forward (reg &optional lim submatch)
-  "Moves to the first not commented occurrence of REG found looking down.  The point
+  "Moves to the first not commented occurrence of REG found looking down.
+The point
 is put exactly before the occurrence if SUBMATCH is nil, otherwise the point is put
 before SUBMATCHnth matched sub-expression (see `match-string').  If no occurrence is
 found, go as far as possible and return nil."
   (coq-find-comment-end)
-  (let ((found nil) (continue t) 
+  (let ((found nil) (continue t)
         (regexp (concat coq-comment-start-regexp "\\|" reg)))
     (while (and (not found) continue)
       (setq continue (re-search-forward regexp lim 'dummy))
@@ -201,25 +215,28 @@ found, go as far as possible and return nil."
     (when found (point))))
 
 (defun coq-find-command-end-backward ()
-  "Moves to the first end of command (not commented) found looking up.  The point is
-put exactly before the last \".\" of the ending token.  If no end command is found,
-go as far as possible and return nil."
+  "Move to the first end of command (not commented) found looking up.
+Point is put exactly before the last \".\" of the ending token.
+If no end command is found, go as far as possible and return
+nil."
   (ignore-errors (forward-char 1)); because regexp looks one char after last "."
   (coq-find-not-in-comment-backward coq-end-command-regexp nil 1))
 
 
 (defun coq-find-command-end-forward ()
-  "Moves to the first end of command found looking down.  The point is put exactly
-before the last \".\" of the ending token.  If no end command is found, go as far as
-possible and return nil."
+  "Move to the first end of command found looking down.
+The point is put exactly before the last \".\" of the ending
+token.  If no end command is found, go as far as possible and
+return nil."
   (ignore-errors (backward-char 1)); because regexp looks one char before "."
   (coq-find-not-in-comment-forward coq-end-command-regexp nil 1))
 
 
 (defun coq-find-command-end (direction)
-  "Moves to the first end of command found looking at direction.  The point is put
-exactly before the last \".\" of the ending token.  If no end command is found, go as
-far as possible and return nil."
+  "Move to the first end of command found looking at DIRECTION.
+The point is put exactly before the last \".\" of the ending
+token.  If no end command is found, go as far as possible and
+return nil."
   (if (< direction 0) (coq-find-command-end-backward)
     (coq-find-command-end-forward)))
 
@@ -227,7 +244,7 @@ far as possible and return nil."
 (defun coq-parse-function ()
   (skip-chars-forward " \n\t")
   (forward-char 1)
-  (if (coq-find-comment-end) 
+  (if (coq-find-comment-end)
       'comment
     (when (coq-find-command-end-forward)
       (forward-char 1)
@@ -257,24 +274,23 @@ The point is put exactly before first non comment letter of the command."
       (buffer-substring st (+ nd 1)))))
 
 (defun only-spaces-on-line ()
-  "t if there is only spaces (or nothing) on the current line after point.
+  "Non-nil if there only spaces (or nothing) on the current line after point.
 Moves point to first non space char if present, to the end of line otherwise."
   (skip-chars-forward " \t" (save-excursion (end-of-line) (point)))
-  (eolp)      
+  (eolp)
   )
 
 
 
 (defun find-reg (lim reg)
-  "Return non nil if there is an occurrence of reg between point and lim which is not
-a comment or a string.  Point is moved at the end of the match if found, at LIM
-otherwise."
+  "Non-nil if REG occurs between point and LIM, not in a comment or string.
+Point is moved at the end of the match if found, at LIM otherwise."
   (let ((oldpt (point)) (limit lim) (found nil))
     (if (= limit (point)) nil
       ;;swap limit and point if necessary
 ;      (message "find-reg...")
       (when (< limit (point)) (let ((x limit)) (setq limit (point)) (goto-char x)))
-      (prog1 
+      (prog1
           (coq-find-not-in-comment-forward reg limit)
         (goto-char (match-end 0))))))
 
@@ -294,11 +310,13 @@ this case)."
 
 
 (defun coq-back-to-indentation-prevline ()
-  "Moves point back to previous pertinent line for indentation. Move point to the
-first non white space character. Returns 0 if top of buffer was reached, 3 if inside
-a comment or string, 4 if inside the {} of a record, 1 if the line found is not in
-the same command as the point before the function was called, 2 otherwise (point and
-previous line are in the same command, and not inside the {} of a record)."
+  "Move point back to previous pertinent line for indentation.
+Move point to the first non white space character.  Returns 0 if
+top of buffer was reached, 3 if inside a comment or string, 4 if
+inside the {} of a record, 1 if the line found is not in the same
+command as the point before the function was called, 2
+otherwise (point and previous line are in the same command, and
+not inside the {} of a record)."
 
   (if (coq-looking-at-syntactic-context) 3
     (let ((oldpt (point))
@@ -320,44 +338,44 @@ previous line are in the same command, and not inside the {} of a record)."
         ; if there is a "." alone on the line
         (let ((pos (point)))
           (ignore-errors (forward-char -1))
-          (if (find-reg oldpt coq-end-command-regexp) 
+          (if (find-reg oldpt coq-end-command-regexp)
               (progn (forward-char -2)
                      (coq-find-real-start)
                      (back-to-indentation)
                      1)
             (goto-char pos)
-            (if (save-excursion 
+            (if (save-excursion
                   (and (or (forward-char -1) t)
                        (coq-find-real-start)
                        (proof-looking-at-safe "Record")
-                       (find-reg oldpt "{"))) 
-                4 
+                       (find-reg oldpt "{")))
+                4
               2)))))))
 
 
 (defun coq-find-unclosed (&optional optlvl limit openreg closereg)
-  "finds the first unclosed open item (backward), counter starts to optlvl (default 1) and stops when reaching limit (default point-min)"
+  "Finds the first unclosed open item (backward), counter starts to optlvl (default 1) and stops when reaching limit (default point-min)."
   
   (let* ((lvl (or optlvl 1))
-			(open-re  (if openreg (proof-regexp-alt openreg proof-indent-open-regexp) 
+			(open-re  (if openreg (proof-regexp-alt openreg proof-indent-open-regexp)
 							proof-indent-open-regexp))
-			(close-re (if closereg (proof-regexp-alt closereg proof-indent-close-regexp) 
+			(close-re (if closereg (proof-regexp-alt closereg proof-indent-close-regexp)
 							proof-indent-close-regexp))
 			(both-re (proof-regexp-alt "\\`" close-re open-re))
 			(nextpt (save-excursion (proof-re-search-backward both-re))))
-    (while 
+    (while
         (and (not (= lvl 0))
              (>= nextpt (or limit (point-min)))
              (not (= nextpt (point-min))))
       (goto-char nextpt)
       (cond
        ((proof-looking-at-syntactic-context) ())
-		 ((proof-looking-at-safe proof-indent-close-regexp) 
+		 ((proof-looking-at-safe proof-indent-close-regexp)
 		  (coq-find-unclosed 1 limit)) ;; recursive call
        ((proof-looking-at-safe close-re) (setq lvl (+ lvl 1)))
        ((proof-looking-at-safe open-re) (setq lvl (- lvl 1))))
       (setq nextpt (save-excursion (proof-re-search-backward both-re))))
-    (if (= lvl 0) t 
+    (if (= lvl 0) t
 		(goto-char (or limit (point-min)))
       nil)))
 
@@ -368,23 +386,23 @@ previous line are in the same command, and not inside the {} of a record)."
 (defun coq-find-at-same-level-zero (limit openreg)
   "Moves to first open or openreg (first found) that is at same parethesis level than point. Returns the point if found."
   (let* ((found nil)
-			(open-re (if openreg (proof-regexp-alt openreg proof-indent-open-regexp) 
+			(open-re (if openreg (proof-regexp-alt openreg proof-indent-open-regexp)
 						  proof-indent-open-regexp))
 			(close-re proof-indent-close-regexp)
 			(both-re (proof-regexp-alt "\\`" close-re open-re))
-			(nextpt (save-excursion (proof-re-search-backward both-re))))  
+			(nextpt (save-excursion (proof-re-search-backward both-re))))
 
-	 (while 
+	 (while
         (and (not found)
              (>= nextpt (or limit (point-min)))
              (not (= nextpt (point-min))))
 		(goto-char nextpt)
-		(cond 
+		(cond
 		 ((proof-looking-at-syntactic-context) ())
        ((proof-looking-at-safe openreg) (setq found t))
        ((proof-looking-at-safe proof-indent-open-regexp) (setq found t));assert false?
 ;       ((proof-looking-at-safe closereg) (coq-find-unclosed 1 limit))
-       ((proof-looking-at-safe proof-indent-close-regexp) 
+       ((proof-looking-at-safe proof-indent-close-regexp)
 		  (coq-find-unclosed 1 limit)))
 		(setq nextpt (save-excursion (proof-re-search-backward both-re)))
 		)
@@ -394,49 +412,45 @@ previous line are in the same command, and not inside the {} of a record)."
 
 
 (defun coq-find-unopened (&optional optlvl limit)
-  "Finds the last unopened close item (looking forward from point), counter starts to optlvl (default 1) and stops when reaching limit (default point-max). This function only works inside an expression."
+  "Finds the last unopened close item (looking forward from point), counter starts to OPTLVL (default 1) and stops when reaching limit (default point-max). This function only works inside an expression."
   
   (let ((lvl (or optlvl 1)) after nextpt endpt)
-	 (save-excursion 
-		(proof-re-search-forward
-		 (proof-regexp-alt "\\'"
-								 proof-indent-close-regexp 
-								 proof-indent-open-regexp))
-		(setq after (point))
-		(goto-char (match-beginning 0))
-		(setq nextpt (point)))
-    (while 
+    (save-excursion
+      (proof-re-search-forward
+       (proof-regexp-alt "\\'"
+                         proof-indent-close-regexp
+                         proof-indent-open-regexp))
+      (setq after (point))
+      (goto-char (match-beginning 0))
+      (setq nextpt (point)))
+    (while
         (and (not (= lvl 0))
              (<= nextpt (or limit (point-max)))
              (not (= nextpt (point-max))))
       (goto-char nextpt)
-		(setq endpt (point))
+      (setq endpt (point))
       (cond
        ((proof-looking-at-syntactic-context) ())
        
-       ((proof-looking-at-safe proof-indent-close-regexp) 
+       ((proof-looking-at-safe proof-indent-close-regexp)
         (setq lvl (- lvl 1)))
        
-       ((proof-looking-at-safe proof-indent-open-regexp) 
-        (setq lvl (+ lvl 1)))
-       
-       )
-		(goto-char after)
+       ((proof-looking-at-safe proof-indent-open-regexp)
+        (setq lvl (+ lvl 1))))
+
+      (goto-char after)
       (save-excursion
 		  (proof-re-search-forward
 			(proof-regexp-alt "\\'"
-									proof-indent-close-regexp 
-									proof-indent-open-regexp))
+                                          proof-indent-close-regexp
+                                          proof-indent-open-regexp))
 		  (setq after (point))
 		  (goto-char (match-beginning 0))
-		  (setq nextpt (point)))
-      )
+		  (setq nextpt (point))))
     (if (= lvl 0)
-		  (goto-char endpt)
+        (goto-char endpt)
       (goto-char (or limit (point-max)))
-      nil)
-    )
-  )
+      nil)))
 
 
 
@@ -445,40 +459,35 @@ previous line are in the same command, and not inside the {} of a record)."
   (let ((last nil))
 	 (while (coq-find-unopened optlvl limit)
 		(setq last (point))
-		(forward-char 1)); shift one to the right, 
+		(forward-char 1)); shift one to the right,
                        ; that way the current match won'tbe matched again
 	 (if last (goto-char last))
-	 last
-	 )
-  )
+	 last))
 
 
 (defun coq-end-offset (&optional limit)
-  "Find the first unclosed open indent item, and returns its column. Stop when reaching limit (defaults tp point-min)"
+  "Find the first unclosed open indent item, and returns its column. Stop when reaching limit (defaults tp point-min)."
   (save-excursion
-    (let ((found nil) 
+    (let ((found nil)
           (anyreg (proof-regexp-alt "\\`" proof-indent-any-regexp)))
-      (while 
+      (while
           (and (not found)
                (> (point) (or limit (point-min))))
         (proof-re-search-backward anyreg)
         (cond
          ((proof-looking-at-syntactic-context) ())
        
-         ((proof-looking-at-safe proof-indent-close-regexp) 
+         ((proof-looking-at-safe proof-indent-close-regexp)
           (coq-find-unclosed))
        
          ((proof-looking-at-safe proof-indent-open-regexp)
           (setq found t))
        
-         (t ())
-         )
-        )
+         (t ())))
+
       (if found (current-column)
         -1000)                          ; no unclosed found
-      )
-    )
-  )
+      )))
 
 
 (defun coq-indent-command-offset (kind prevcol prevpoint)
@@ -489,7 +498,7 @@ previous line are in the same command, and not inside the {} of a record)."
 
    ;; we are at an end command -> one ident left
    ;; FIX: we should count the number of closing item on the line
-   ((coq-save-command-p nil (or (coq-command-at-point) "")) 
+   ((coq-save-command-p nil (or (coq-command-at-point) ""))
     (- proof-indent))
 
 
@@ -504,7 +513,7 @@ previous line are in the same command, and not inside the {} of a record)."
              ))
     proof-indent)
 
-;;	((and (goto-char prevpoint) 
+;;	((and (goto-char prevpoint)
 ;;         ;"Proof <term>." is actually a Save command
 ;;         ; catched only if not follwed by"." or "with"
 ;;			(proof-looking-at-safe "\\<Proof\\>"))
@@ -535,116 +544,113 @@ This function indents a *expression* line (a line inside of a command).  Use
 argument must be t if inside the {}s of a record, nil otherwise."
 
   (let ((pt (point)) real-start)
-	 (save-excursion 
-		(setq real-start (coq-find-real-start)))
+    (save-excursion
+      (setq real-start (coq-find-real-start)))
   
-	 (cond
-
-  ; at a ) -> same indent as the *line* of corresponding (
-	  ((proof-looking-at-safe coq-indent-closepar-regexp)
-		(save-excursion (coq-find-unclosed 1 real-start)
-							 (back-to-indentation)
-							 (current-column)))
-
-  ; at a end -> same indent as the corresponding match or Case
-	  ((proof-looking-at-safe coq-indent-closematch-regexp)
-     (save-excursion (coq-find-unclosed 1 real-start)
-                     (current-column)))
-
-  ; if we find a "|" we indent from the first unclosed 
-  ; or from the command start (if we are in an Inductive type)
-	  ((proof-looking-at-safe coq-indent-pattern-regexp) 
-     (save-excursion 
-       (coq-find-unclosed 1 real-start)
-       (cond 
-        ((proof-looking-at-safe "\\s(")
-         (+ (current-indentation) proof-indent))
-        ((proof-looking-at-safe (proof-ids-to-regexp coq-keywords-defn))
-         (current-column))
+    (cond
+
+     ;; at a ) -> same indent as the *line* of corresponding (
+     ((proof-looking-at-safe coq-indent-closepar-regexp)
+      (save-excursion (coq-find-unclosed 1 real-start)
+                      (back-to-indentation)
+                      (current-column)))
+
+     ;; at an end -> same indent as the corresponding match or Case
+     ((proof-looking-at-safe coq-indent-closematch-regexp)
+      (save-excursion (coq-find-unclosed 1 real-start)
+                      (current-column)))
+
+     ;; if we find a "|" we indent from the first unclosed
+     ;; or from the command start (if we are in an Inductive type)
+     ((proof-looking-at-safe coq-indent-pattern-regexp)
+      (save-excursion
+        (coq-find-unclosed 1 real-start)
+        (cond
+         ((proof-looking-at-safe "\\s(")
+          (+ (current-indentation) proof-indent))
+         ((proof-looking-at-safe (proof-ids-to-regexp coq-keywords-defn))
+          (current-column))
          (t (+ (current-column) proof-indent)))))
 
-  ; if we find a "then" we indent from the first unclosed if
-  ; or from the command start (should not happen)
-	  ((proof-looking-at-safe "\\<then\\>") 
-		(save-excursion
-		  (coq-find-unclosed 1 real-start "\\<if\\>" "\\<then\\>")
-		  (back-to-indentation)
-		  (+ (current-column) proof-indent)))
-
-  ; if we find a "else" we indent from the first unclosed if
-  ; or from the command start (should not happen)
-	  ((proof-looking-at-safe "\\<else\\>") 
-		(save-excursion
-		  (coq-find-unclosed 1 real-start "\\<then\\>" "\\<else\\>")
-		  (coq-find-unclosed 1 real-start "\\<if\\>" "\\<then\\>")
-		  (back-to-indentation)
-		  (+ (current-column) proof-indent)))
-
-  ; there is an unclosed open in the previous line 
-  ; -> same column if match
-  ; -> same indent than prev line + indent if (
-	  ((coq-find-unclosed 1 prevpoint
-								 coq-indent-openmatch-regexp 
-								 coq-indent-closematch-regexp)
-		(let ((base (if (proof-looking-at-safe coq-indent-openmatch-regexp)
-							 (current-column)
-						  prevcol)))
-		  (+ base proof-indent)))
-
-
-; there is an unclosed '(' in the previous line -> prev line indent + indent
-;	  ((and (goto-char pt) nil)) ; just for side effect: jump to initial point
-;	  ((coq-find-unclosed 1 prevpoint 
-;								 coq-indent-openpar-regexp 
-;								 coq-indent-closepar-regexp)
-;		(+ prevcol proof-indent))
-
-	  ((and (goto-char prevpoint) nil)) ; just for side effect: jump to previous line
-	
-; find the last unopened ) -> indentation of line + indent
-	  ((coq-find-last-unopened 1 pt) ; side effect, nil if no unopenned found
-		(save-excursion
-		  (coq-find-unclosed 1 real-start)
-		  (back-to-indentation)
-		  (current-column)))
-
-; just for side effect: jumps to end of previous line
-	  ((and (goto-char prevpoint) 
-			  (or (and (end-of-line) nil) 
-					(and (forward-char -1) t)) nil))
-
-	  ((and  (proof-looking-at-safe ";") ;prev line has ";" at the end 
-				record)                     ; and we are inside {}s of a record
-		(save-excursion (coq-find-unclosed 1 real-start)
-							 (back-to-indentation)
-							 (+ (current-column) proof-indent)))
-
-; just for side effect: jumps to end of previous line
-	  ((and (goto-char prevpoint)  (not (= (coq-back-to-indentation-prevline) 0))
-			  (or (and (end-of-line) nil) 
-					(and (forward-char -1) t)) nil))
-
-	  ((and  (proof-looking-at-safe ";") ;prev prev line has ";" at the end 
-				record)                     ; and we are inside {}s of a record
-		(save-excursion (+ prevcol proof-indent)))
-
-
-	  ((and (goto-char pt) nil)) ; just for side effect: go back to initial point
-
-; There is a indent keyword (fun, forall etc) 
-; and we are not in {}s of a record just after a ";"
-	  ((coq-find-at-same-level-zero prevpoint coq-indent-kw) (+ prevcol proof-indent))
-
-	  ((and (goto-char prevpoint) nil)) ; just for side effect: go back to previous line
-
-; "|" at previous line
-	  ((proof-looking-at-safe coq-indent-pattern-regexp) (+ prevcol proof-indent))
-
-	  (t prevcol)
-	  )
-	 )
-  )
+     ;; if we find a "then" we indent from the first unclosed if
+     ;; or from the command start (should not happen)
+     ((proof-looking-at-safe "\\<then\\>")
+      (save-excursion
+        (coq-find-unclosed 1 real-start "\\<if\\>" "\\<then\\>")
+        (back-to-indentation)
+        (+ (current-column) proof-indent)))
 
+     ;; if we find a "else" we indent from the first unclosed if
+     ;; or from the command start (should not happen)
+     ((proof-looking-at-safe "\\<else\\>")
+      (save-excursion
+        (coq-find-unclosed 1 real-start "\\<then\\>" "\\<else\\>")
+        (coq-find-unclosed 1 real-start "\\<if\\>" "\\<then\\>")
+        (back-to-indentation)
+        (+ (current-column) proof-indent)))
+
+     ;; there is an unclosed open in the previous line
+     ;; -> same column if match
+     ;; -> same indent than prev line + indent if (
+     ((coq-find-unclosed 1 prevpoint
+                         coq-indent-openmatch-regexp
+                         coq-indent-closematch-regexp)
+      (let ((base (if (proof-looking-at-safe coq-indent-openmatch-regexp)
+                      (current-column)
+                    prevcol)))
+        (+ base proof-indent)))
+
+
+;; there is an unclosed '(' in the previous line -> prev line indent + indent
+;;	  ((and (goto-char pt) nil)) ; just for side effect: jump to initial point
+;;	  ((coq-find-unclosed 1 prevpoint
+;;            coq-indent-openpar-regexp
+;;            coq-indent-closepar-regexp)
+;;		(+ prevcol proof-indent))
+
+     ((and (goto-char prevpoint) nil)) ; just for side effect: jump to previous line
+	
+     ;; find the last unopened ) -> indentation of line + indent
+     ((coq-find-last-unopened 1 pt) ; side effect, nil if no unopenned found
+      (save-excursion
+        (coq-find-unclosed 1 real-start)
+        (back-to-indentation)
+        (current-column)))
+
+     ;; just for side effect: jumps to end of previous line
+     ((and (goto-char prevpoint)
+           (or (and (end-of-line) nil)
+               (and (forward-char -1) t)) nil))
+     
+     ((and  (proof-looking-at-safe ";") ;prev line has ";" at the end
+            record)                     ; and we are inside {}s of a record
+      (save-excursion 
+        (coq-find-unclosed 1 real-start)
+        (back-to-indentation)
+        (+ (current-column) proof-indent)))
+
+     ;; just for side effect: jumps to end of previous line
+     ((and (goto-char prevpoint)  (not (= (coq-back-to-indentation-prevline) 0))
+           (or (and (end-of-line) nil)
+               (and (forward-char -1) t)) nil))
+     
+     ((and (proof-looking-at-safe ";") ;prev prev line has ";" at the end
+           record)                     ; and we are inside {}s of a record
+      (save-excursion (+ prevcol proof-indent)))
+
+     ((and (goto-char pt) nil)) ;; just for side effect: go back to initial point
+
+     ;; There is a indent keyword (fun, forall etc)
+     ;; and we are not in {}s of a record just after a ";"
+     ((coq-find-at-same-level-zero prevpoint coq-indent-kw) 
+      (+ prevcol proof-indent))
+
+     ((and (goto-char prevpoint) nil)) ;; just for side effect: go back to previous line
+     ;; "|" at previous line
+     ((proof-looking-at-safe coq-indent-pattern-regexp)
+      (+ prevcol proof-indent))
+     
+     (t prevcol)))
 
 
 (defun coq-indent-comment-offset ()
@@ -661,7 +667,7 @@ argument must be t if inside the {}s of a record, nil otherwise."
         (let ((eol (save-excursion (end-of-line) (point))))
         (cond
          ;; The previous line contains is the comment start
-         ((and (not atstart) (string-match coq-comment-start-regexp 
+         ((and (not atstart) (string-match coq-comment-start-regexp
                                            (buffer-substring (point) eol)))
           (re-search-forward coq-comment-start-regexp) ;first '(*' in the line?
           (+ 1 (current-column)))
@@ -681,29 +687,29 @@ argument must be t if inside the {}s of a record, nil otherwise."
 
 (defun coq-indent-offset (&optional notcomments)
   (let (kind prevcol prevpoint)
-	 (save-excursion
-		(setq kind (coq-back-to-indentation-prevline) ;go to previous *command* (assert)
-				prevcol (current-column)
-				prevpoint (point)))
-;   (message "coq-indent-offset... kind = %s ; prevcol = %s; prevpoint = %s" kind prevcol prevpoint)
-	 (cond 
+    (save-excursion
+      (setq kind (coq-back-to-indentation-prevline) ;go to previous *command* (assert)
+            prevcol (current-column)
+            prevpoint (point)))
+    ;;   (message "coq-indent-offset... kind = %s ; prevcol = %s; prevpoint = %s" kind prevcol prevpoint)
+	 (cond
 	  ((= kind 0) 0) ; top of the buffer reached
 	  ((= kind 1) ; we are at the command level
-     (+ prevcol (coq-indent-command-offset kind prevcol prevpoint)))
+           (+ prevcol (coq-indent-command-offset kind prevcol prevpoint)))
 	  ((= kind 2) ; we are at the expression level
-     (coq-indent-expr-offset kind prevcol prevpoint nil))
+           (coq-indent-expr-offset kind prevcol prevpoint nil))
 	  ((= kind 4) ; we are at the expression level inside {}s of a record
-     (coq-indent-expr-offset kind prevcol prevpoint t))
-	  ((= kind 3) (if notcomments nil (coq-indent-comment-offset))))))
+           (coq-indent-expr-offset kind prevcol prevpoint t))
+	  ((= kind 3) 
+           (if notcomments nil (coq-indent-comment-offset))))))
 
-(defun coq-indent-calculate (&optional notcomments) 
+(defun coq-indent-calculate (&optional notcomments)
   (coq-indent-offset notcomments))
 
-
-(defun proof-indent-line ()
+(defun coq-indent-line ()
   "Indent current line of proof script, if indentation enabled."
   (interactive)
-  (unless (not (proof-ass script-indent))
+  (unless (not coq-script-indent)
     (save-excursion
       (let ((ind (save-excursion (back-to-indentation) (coq-indent-calculate))))
         (indent-line-to (max 0 ind))))
@@ -711,9 +717,9 @@ argument must be t if inside the {}s of a record, nil otherwise."
         (back-to-indentation))))
 
 (defun coq-indent-line-not-comments ()
-  "Same as  `proof-indent-line' but comments are not indented."
+  "Same as  `coq-indent-line' but comments are not indented."
   (interactive)
-  (unless (not (proof-ass script-indent))
+  (unless (not coq-script-indent)
     (save-excursion
       (let ((ind (save-excursion (back-to-indentation) (coq-indent-calculate t))))
         (when ind (indent-line-to (max 0 ind)))))
@@ -723,7 +729,7 @@ argument must be t if inside the {}s of a record, nil otherwise."
 (defun coq-indent-region (start end)
   (let ((deb (min start end)) (fin (max start end)))
     (goto-char end)
-    (setq fin (point-marker)) ; to go back there even if shifted
+    (setq fin (point-marker)) ;; to go back there even if shifted
     (goto-char deb)
     (while (< (point) fin)
       (or (and (bolp) (eolp))
@@ -739,3 +745,7 @@ argument must be t if inside the {}s of a record, nil otherwise."
 ;;;   indent-tabs-mode:nil ***
 ;;;   End: ***
 
+
+(provide 'coq-indent)
+
+;;; coq-indent.el ends here