indentation for coq completely re-coded, because the generic mechanism

does not use "proof-goal-command-p" and is not powerful enough.

5 files changed, 708 insertions, 168 deletions

diff --git a/coq/coq-abbrev.el b/coq/coq-abbrev.el
index 14626227..8e7fff66 100644
--- a/coq/coq-abbrev.el
+++ b/coq/coq-abbrev.el
@@ -77,10 +77,10 @@
 		("inf" "infix \"#\" := # (at level #) : #." holes-abbrev-complete 1)
 		("ind" "induction #" holes-abbrev-complete 2)
 		("indv" "Inductive # : # := # : #." holes-abbrev-complete 0)
-		("indv2" "Inductive # : # :=\n# : #\n| # : #." holes-abbrev-complete 0)
-		("indv3" "Inductive # : # :=\n  # : #\n| # : #\n| # : #." holes-abbrev-complete 0)
-		("indv4" "Inductive # : # :=\n  # : #\n| # : #\n| # : #\n| # : #." holes-abbrev-complete 0)
-		("indv5" "Inductive # : # :=\n  # : #\n| # : #\n| # : #\n| # : #\n| # : #." holes-abbrev-complete 0)
+		("indv2" "Inductive # : # :=\n| # : #\n| # : #." holes-abbrev-complete 0)
+		("indv3" "Inductive # : # :=\n| # : #\n| # : #\n| # : #." holes-abbrev-complete 0)
+		("indv4" "Inductive # : # :=\n| # : #\n| # : #\n| # : #\n| # : #." holes-abbrev-complete 0)
+		("indv5" "Inductive # : # :=\n| # : #\n| # : #\n| # : #\n| # : #\n| # : #." holes-abbrev-complete 0)
 		("inj" "injection #" holes-abbrev-complete 2)
 		("inv" "inversion #" holes-abbrev-complete 9)
 		("intu" "intuition #" holes-abbrev-complete 9)
@@ -88,11 +88,11 @@
 		("ite" "if # then # else #" holes-abbrev-complete 1)
 		("l" "Lemma # : #." holes-abbrev-complete 4)
 		("li" "let # := # in #" holes-abbrev-complete 1)
-		("m" "match # with\n# => #\nend" holes-abbrev-complete 1)
-		("m2" "match # with\n # => #\n| # => #\nend" holes-abbrev-complete 1)
-		("m3" "match # with\n  # => #\n| # => #\n| # => #\nend" holes-abbrev-complete 1)
-		("m4" "match # with\n# => #\n| # => #\n| # => #\n| # => #\nend" holes-abbrev-complete 1)
-		("m5" "match # with\n  # => #\n| # => #\n| # => #\n| # => #\n| # => #\nend" holes-abbrev-complete 1)
+		("m" "match # with\n| # => #\nend" holes-abbrev-complete 1)
+		("m2" "match # with\n| # => #\n| # => #\nend" holes-abbrev-complete 1)
+		("m3" "match # with\n| # => #\n| # => #\n| # => #\nend" holes-abbrev-complete 1)
+		("m4" "match # with\n| # => #\n| # => #\n| # => #\n| # => #\nend" holes-abbrev-complete 1)
+		("m5" "match # with\n| # => #\n| # => #\n| # => #\n| # => #\n| # => #\nend" holes-abbrev-complete 1)
 		("mt" "Module Type # := #." holes-abbrev-complete 0)
 		("mti" "Module Type #.\n#\nEnd #." holes-abbrev-complete 0)
 		("mo" "Module # : # := #." holes-abbrev-complete 0)
diff --git a/coq/coq-indent.el b/coq/coq-indent.el
new file mode 100644
index 00000000..c47e2afa
--- /dev/null
+++ b/coq/coq-indent.el
@@ -0,0 +1,529 @@
+;; coq-syntax.el indentation stuff for Coq
+;; 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.
+
+
+(require 'coq-syntax)
+
+(defconst coq-any-command-regexp
+  (proof-regexp-alt (proof-ids-to-regexp coq-keywords)))
+
+
+(defconst coq-indent-inner-regexp
+  (proof-regexp-alt "[[]()]" "|"
+						  (proof-ids-to-regexp   '("as"
+;															"ALL"
+;															"True"
+;															"False"
+															"Cases"
+															"match"
+;															"EX"
+															"else"
+;															"end"
+															"Fix"
+															"forall"
+															"fun"
+															"if"
+;															"in"
+															"into"
+															"let"
+;															"of"
+															"then"
+															"using"
+;															"with"
+															"after"))))
+
+
+(defconst coq-indent-open-regexp
+  (proof-regexp-alt ;(proof-ids-to-regexp coq-keywords-goal) goal-command-p instead
+	(proof-ids-to-regexp '("Cases" "match"))
+	"\\s("))
+
+(defconst coq-indent-close-regexp
+  (proof-regexp-alt (proof-ids-to-regexp coq-keywords-save) 
+						  (proof-ids-to-regexp '("end" "End"))
+						  "\\s)"))
+
+(defconst coq-indent-closepar-regexp "\\s)")
+
+(defconst coq-indent-closematch-regexp (proof-ids-to-regexp '("end")))
+
+(defconst coq-indent-openpar-regexp "\\s(")
+
+(defconst coq-indent-openmatch-regexp (proof-ids-to-regexp '("match" "Cases")))
+
+(defconst coq-indent-any-regexp
+  (proof-regexp-alt 
+	coq-indent-close-regexp 
+	coq-indent-open-regexp 
+	coq-indent-inner-regexp 
+	coq-any-command-regexp 
+	(proof-ids-to-regexp coq-tacticals)
+	(proof-ids-to-regexp coq-tactics)))
+
+(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)))
+
+; pattern matching detection, will be tested only at beginning of a
+;line (only white sapces before "|") must not match "|" followed by
+;another symbol the following char must not be a symbol (tokens of coq
+;are the biggest symbol cocateantions)
+
+(defconst coq-indent-pattern-regexp "|\\(?:\\s-\\|\\w\\|\n\\)")
+
+;;;; End of regexps
+
+
+(defun coq-find-command-start ()
+  (proof-re-search-backward "\\.\\B\\|\\`")
+  (while (and (proof-looking-at-syntactic-context)
+				  (> (point) (point-min)))
+    (proof-re-search-backward "\\.\\B\\|\\`"))
+  (if (proof-looking-at "\\.\\B") (forward-char 1))
+  (point)
+  )
+
+(defun coq-find-real-start ()
+  (coq-find-command-start)
+  (proof-re-search-forward "\\w\\|\\s(\\|\\s)\\|\\'")
+  (backward-char 1)
+  (while (and (proof-looking-at-syntactic-context)
+				  (<= (point) (- (point-max) 1)))
+    (proof-re-search-forward "\\*\\s)");this does not deal with nested comments
+    (proof-re-search-forward "\\w\\|\\s(\\|\\s)\\|\\'")
+    (backward-char 1))
+  (point)
+  )
+
+(defun coq-find-end ()
+  (proof-re-search-forward "\\.\\B\\|\\'")
+  (while (and (proof-looking-at-syntactic-context)
+				  (<= (point) (point-max)))
+    (proof-re-search-forward "\\*\\s)")
+    (proof-re-search-forward "\\.\\B\\|\\'"))
+;  (backward-char 1)
+  (point)
+  )
+
+(defun coq-current-command-string ()
+  (save-excursion
+    (let ((st (coq-find-real-start)) ; va chercher trop loin?
+          (nd (coq-find-end))) ; idem?
+      (buffer-substring st nd))
+    )
+  )
+
+(defun is-at-a-space-or-tab ()
+  "t si le caractere courant est un blanc ou un tab, nil sinon"
+  (if (or (not (char-after)) (char-equal (char-after) ?\ ) (char-equal (char-after) ?\t ))
+      t nil)
+  )
+
+(defun only-spaces-on-line ()
+  "t if there is only spaces (or nothing) on the current line after point"
+  (while (and (char-after) (is-at-a-space-or-tab))
+    (forward-char 1))
+  (if (or (not (char-after)) (char-equal (char-after) ?\n)) t nil)
+)
+
+(defun find-reg (limit reg)
+  (if (< limit (point))
+      (let (x limit) (setq limit (point)) (goto-char x)))
+  (let ((pos nil))
+    (while 
+        (and (not pos)
+             (setq pos (proof-string-match reg (buffer-substring (point) limit))))
+      (forward-char pos)
+      (if (proof-looking-at-syntactic-context) (setq pos nil)))
+    pos)
+  )
+
+(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)."
+
+  (if (proof-looking-at-syntactic-context) 3
+	 (let ((oldpt (point))
+			 (topnotreached (= (forward-line -1) 0))) ; nil if going one line backward
+													 ; is not possible
+		(while (and topnotreached
+						(or (only-spaces-on-line) (proof-looking-at-syntactic-context))
+						t ;(> (line-number (point)) (line-number (point-min)))
+						)
+		  (setq topnotreached (= (forward-line -1) 0)))
+		(back-to-indentation)
+		(if (not topnotreached) 0 ; returns nil if top of buffer was reached
+		  (if (find-reg oldpt "\\.\\B");; if we are at end of a command (dot) find this command
+				(progn (coq-find-real-start) 1)
+			 (if (save-excursion 
+					 (coq-find-real-start) 
+					 (proof-looking-at-safe "Record")
+					 (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)"
+  
+  (let* ((lvl (or optlvl 1))
+			(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) 
+							proof-indent-close-regexp))
+			(both-re (proof-regexp-alt "\\`" close-re open-re))
+			(nextpt (save-excursion (proof-re-search-backward both-re))))
+    (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) 
+		  (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 
+		(goto-char (or limit (point-min)))
+      nil)))
+
+
+(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) 
+						  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))))  
+
+	 (while 
+        (and (not found)
+             (>= nextpt (or limit (point-min)))
+             (not (= nextpt (point-min))))
+		(goto-char nextpt)
+		(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) 
+		  (coq-find-unclosed 1 limit)))
+		(setq nextpt (save-excursion (proof-re-search-backward both-re)))
+		)
+	 (if found (point) nil)
+	 )
+  )
+
+
+(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."
+  
+  (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 
+        (and (not (= lvl 0))
+             (<= nextpt (or limit (point-max)))
+             (not (= nextpt (point-max))))
+      (goto-char nextpt)
+		(setq endpt (point))
+      (cond
+       ((proof-looking-at-syntactic-context) ())
+       
+       ((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)
+      (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)))
+      )
+    (if (= lvl 0)
+		  (goto-char endpt)
+      (goto-char (or limit (point-max)))
+      nil)
+    )
+  )
+
+
+(defun coq-find-last-unopened (&optional optlvl limit)
+  "Backward moves to and returns the point of the last close item that is not opened after limit."
+  (let ((last nil))
+	 (while (coq-find-unopened optlvl limit)
+		(setq last (point))
+		(forward-char 1)); shift one to the right, 
+                       ; that way the current match won'tbe matched again
+	 (if last (goto-char 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)"
+  (save-excursion
+    (let ((found nil) (cpt 0) (found nil) 
+          (anyreg (proof-regexp-alt "\\`" proof-indent-any-regexp)))
+      (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) 
+          (coq-find-unclosed))
+       
+         ((proof-looking-at-safe proof-indent-open-regexp)
+          (setq found t))
+       
+         (t ())
+         )
+        )
+      (if found (current-column)
+        -1000)                          ; no unclosed found
+      )
+    )
+  )
+
+
+(defun coq-indent-command-offset (kind prevcol prevpoint)
+  "Returns the indentation offset of the current line. This function indents a *command* line (the first line of a command). Use `coq-indent-expr-offset' to indent a line belonging to an expression."
+  (cond
+
+  ; 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 (coq-current-command-string)) 
+	 (- proof-indent))
+
+	((proof-looking-at-safe "\\<Proof\\>") 0) ; no indentation at "Proof ..."
+
+  ; previous command is a goal command -> one indent right
+  ; carreful: this line moves the point
+	((and (goto-char prevpoint) 
+			(or (and ;"Proof ..." is a proof start (but not really a goal command)
+                  ;  unless followed by a term (catch by coq-save-command-p above
+				  (proof-looking-at-safe "\\<Proof\\>")
+				  (not (coq-save-command-p (coq-current-command-string))))
+				 (coq-goal-command-p (coq-current-command-string))))
+	 proof-indent)
+
+;	((and (goto-char prevpoint) 
+;         ;"Proof <term>." is actually a Save command
+;         ; catched only if not follwed by"." or "with"
+;			(proof-looking-at-safe "\\<Proof\\>"))
+;	 (- proof-indent))
+
+
+  ; otherwise -> same indent as previous command
+	(t 0)
+	)
+  )
+
+
+
+;; This function is very complex, indentation of a line (inside an
+;; expression) is determined by the beginning of this line (current
+;; point) and the indentation items found at previous pertinent (not
+;; comment, not string, not empty) line. Sometimes we even need the
+;; previous line of previous line.
+
+;; prevcol is the indentation column of the previous line, prevpoint
+;; is the indetation point of previous line, record tells if we are
+;; inside a the accolades of a record.
+
+(defun coq-indent-expr-offset (kind prevcol prevpoint record)
+  "Returns the indentation column of the current line. This function indents a *expression* line (a line inside of a command). Use `coq-indent-command-offset' to indent a line belonging to a command. The fourth argument must be t if inside the {}s of a record, nil otherwise."
+
+  (let ((pt (point)) real-start unclosed)
+	 (save-excursion
+		(setq unclosed (coq-find-unclosed 1 prevpoint)))
+	 (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)
+							 (+ (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)
+	  )
+	 )
+  )
+
+
+
+(defun coq-indent-offset ()
+  (let ((col (current-column)) kind prevpt prevcol)
+	 (save-excursion
+		(setq kind (coq-back-to-indentation-prevline) ;go to previous *command* (assert)
+				prevcol (current-column)
+				prevpoint (point)))
+	 (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)))
+	  ((= kind 2) ; we are at the expression level
+		(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) (+ (current-column) 2))
+	  )
+		
+	 )
+  )
+
+(defun coq-indent-calculate () 
+  (coq-indent-offset)
+
+;  (let ((oldpt (point)) (prvfound nil) (res 0))
+;    (setq res
+;          (+ (save-excursion 
+;               (setq prvfound (coq-back-to-indentation-prevline))
+;               (current-column)) ; indentation of previous pertinent line
+;             (coq-indent-offset))) ; + offset for the current line
+;    (if (= prvfound 0) 0 res) ; if we are at buffer top, then 0 else res
+;    )
+  )
+
+
+(defun proof-indent-line ()
+  "Indent current line of proof script, if indentation enabled."
+  (interactive)
+  (unless (not (proof-ass script-indent))
+    (if (< (point) (proof-locked-end))
+        (if (< (current-column) (current-indentation))
+            (skip-chars-forward "\t "))
+      (save-excursion
+        (indent-line-to
+         (max 
+          0 
+          (save-excursion
+            (back-to-indentation)
+            (coq-indent-calculate)))))
+      (if (< (current-column) (current-indentation))
+          (back-to-indentation))))
+  (if proof-indent-pad-eol (proof-indent-pad-eol)))
+
+
+(provide 'coq-indent)
+
diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el
index 09ba5878..3ded2e64 100644
--- a/coq/coq-syntax.el
+++ b/coq/coq-syntax.el
@@ -58,54 +58,56 @@ version of coq by doing 'coqtop -v'."  )
 ;; only coq-version-is-V74 and coq-version-is-V7 are used later (V6
 ;; corresponds to v7=nil and v74=nil)
 
-(unless (noninteractive) ;; DA: evaluating here gives error during compile
-(let* ((seedoc " (to force another version, do for example C-h v coq-version-is-V7)")
-		(v8 (concat "proofgeneral is in coq 8 mode" seedoc))
-		(v74 (concat "proofgeneral is in coq 7.4 mode" seedoc))
-		(v7 (concat "proofgeneral is in coq > 6 and =< 7.3 mode" seedoc))
-		(v6 (concat "proofgeneral is in coq V6 mode" seedoc)))
-  (cond
-   (coq-version-is-V8 
-    (message v8) 
-    (setq coq-version-is-V74 t))
-   (coq-version-is-V74 
-    (message v74) 
-    (setq coq-version-is-V8 nil)
-    (setq coq-version-is-V7 t))
-   (coq-version-is-V7  
-    (message v7)  
-    (setq coq-version-is-V74 nil)
-    (setq coq-version-is-V8 nil))
-   (coq-version-is-V6  
-    (message v6)  
-    (setq coq-version-is-V8 nil) 
-    (setq coq-version-is-V74 nil) 
-    (setq coq-version-is-V7 nil))
-   (t 
-    (let* ((str (shell-command-to-string (concat coq-prog-name " -v")))
-	   ;; da: next line not used?
-	   ;;(x (string-match "version \\([.0-9]*\\)" str))
-	   (num (match-string 1 str)))
-      ;; da: added this to avoid type error in case coq command fails
-      (if (null num) (setq num ""))
-      (cond
-       ((string-match num "\\<6.") 
-	(message v6)
-	(setq coq-version-is-V7 nil) 
-	(setq coq-version-is-V74 nil))
-       ((or (string-match num "\\<7.0") 
-	    (string-match num "\\<7.1") 
-	    (string-match num "\\<7.2") 
-	    (string-match num "\\<7.3")) 
-	(message v7) 
-	(setq coq-version-is-V7 t)
-	(setq coq-version-is-V74 nil))
-       ((string-match num "\\<8"))
-       (t 
-	(message v8) 
-	(setq coq-version-is-V8 t)
-	(setq coq-version-is-V7 t) 
-	(setq coq-version-is-V74 t))))))))
+(unless (noninteractive);; DA: evaluating here gives error during compile
+  (let* ((seedoc " (to force another version, do for example C-h v coq-version-is-V7)")
+			(v8 (concat "proofgeneral is in coq 8 mode" seedoc))
+			(v74 (concat "proofgeneral is in coq 7.4 mode" seedoc))
+			(v7 (concat "proofgeneral is in coq > 6 and =< 7.3 mode" seedoc))
+			(v6 (concat "proofgeneral is in coq V6 mode" seedoc)))
+	 (cond
+	  (coq-version-is-V8 
+		(message v8) 
+		(setq coq-version-is-V74 t))
+	  (coq-version-is-V74 
+		(message v74) 
+		(setq coq-version-is-V8 nil)
+		(setq coq-version-is-V7 t))
+	  (coq-version-is-V7  
+		(message v7)  
+		(setq coq-version-is-V74 nil)
+		(setq coq-version-is-V8 nil))
+	  (coq-version-is-V6  
+		(message v6)  
+		(setq coq-version-is-V8 nil) 
+		(setq coq-version-is-V74 nil) 
+		(setq coq-version-is-V7 nil))
+	  (t 
+		(let* ((str (shell-command-to-string (concat coq-prog-name " -v")))
+				 ;; da: next line not used? Pierre: yes, string-match 1 ... 
+				 ;; at following line returns the last matched regexp (first parenth) 
+				 ;; so we need to make the string-match, and then match-string
+				 (x (string-match "version \\([.0-9]*\\)" str))
+				 (num (match-string 1 str)))
+		  ;; da: added this to avoid type error in case coq command fails
+		  (if (null num) (setq num ""))
+		  (cond
+			((string-match num "\\<6.") 
+			 (message v6)
+			 (setq coq-version-is-V7 nil) 
+			 (setq coq-version-is-V74 nil))
+			((or (string-match num "\\<7.0") 
+				  (string-match num "\\<7.1") 
+				  (string-match num "\\<7.2") 
+				  (string-match num "\\<7.3")) 
+			 (message v7) 
+			 (setq coq-version-is-V7 t)
+			 (setq coq-version-is-V74 nil))
+			((string-match num "\\<8"))
+			(t 
+			 (message v8) 
+			 (setq coq-version-is-V8 t)
+			 (setq coq-version-is-V7 t) 
+			 (setq coq-version-is-V74 t))))))))
 
 ;; ----- keywords for font-lock.
 
@@ -146,7 +148,8 @@ version of coq by doing 'coqtop -v'."  )
 ;; Modules are like section in v > 7.4.
 (if (or coq-version-is-V74 coq-version-is-V8)
 	 (defvar coq-keywords-goal
-		'("Chapter"
+		'("Add\\s-+Morphism"
+		  "Chapter"
 		  "Declare\\s-+Module";;only if not followed by:=(see coq-proof-mode-p in coq.el)
 		  "Module"
 		  "Module\\s-+Type"
@@ -170,6 +173,64 @@ version of coq by doing 'coqtop -v'."  )
 		"Remark"
 		"Section"
 		"Theorem")))
+
+;; FIXME da: this one function breaks the nice configuration of Proof General:
+;; would like to have proof-goal-regexp instead.
+;; Unfortunately Coq allows "Definition" and friends to perhaps have a goal, 
+;; so it appears more difficult than just a proof-goal-regexp setting.
+;; Future improvement may simply to be allow a function value for
+;; proof-goal-regexp.
+
+;; excerpt of Jacek Chrzaszcz, implementer of the module system: sorry
+;; for the french:
+;*) suivant les suggestions de Chritine, pas de mode preuve dans un type de
+;    module (donc pas de Definition truc:machin.  Lemma, Theorem ... )
+;
+; *) la commande Module M [ ( : | <: ) MTYP ] [ := MEXPR ] est valable
+;    uniquement hors d'un MT
+;    - si :=MEXPR est absent, elle demarre un nouveau module interactif
+;    - si :=MEXPR est present, elle definit un module
+;    (la fonction vernac_define_module dans toplevel/vernacentries) 
+;
+; *) la nouvelle commande Declare Module M [ ( : | <: ) MTYP ] [ := MEXPR ]
+;    est valable uniquement dans un MT
+;    - si :=MEXPR absent, :MTYP absent, elle demarre un nouveau module
+;      interactif
+;    - si (:=MEXPR absent, :MTYP present) 
+;      ou (:=MEXPR present, :MTYP absent)
+;      elle declare un module.
+;    (la fonction vernac_declare_module dans toplevel/vernacentries)
+
+(defun coq-count-match (regexp strg)
+  "Count the number of (maximum, non overlapping) matching substring 
+of STRG matching REGEXP. Empty match are counted once."
+  (let ((nbmatch 0) (str strg))
+    (while (and (proof-string-match regexp str) (not (string-equal str "")))
+      (incf nbmatch)
+      (if (= (match-end 0) 0) (setq str (substring str 1))
+        (setq str (substring str (match-end 0)))))
+    nbmatch))
+
+
+
+(defun coq-goal-command-p (str)
+  "Decide whether argument is a goal or not"
+  (let* ((match (coq-count-match "\\<match\\>" str))
+		  (with (coq-count-match "\\<with\\>" str))
+		  (letwith (+ (coq-count-match "\\<let\\>" str) (- with match)))
+		  (affect (coq-count-match ":=" str)))
+		  
+	 (and (proof-string-match coq-goal-command-regexp str)
+			(not									 ; 
+			 (and 
+			  (proof-string-match "\\`\\(Local\\|Definition\\|Lemma\\|Module\\)\\>" str)
+			  (not (= letwith affect))))
+			(not (proof-string-match "\\`Declare\\s-+Module\\(\\w\\|\\s-\\|<\\)*:" str))
+			)
+	 )
+  )
+
+
 (defvar coq-keywords-save
   '("Defined"
     "Save"
@@ -178,6 +239,14 @@ version of coq by doing 'coqtop -v'."  )
 	 "Admitted"
 	 ))
 
+(defun coq-save-command-p (str)
+  "Decide whether argument is a Save command or not"
+  (or (proof-string-match coq-save-command-regexp str)
+		(and (proof-string-match "\\`Proof\\>" str)
+			  (not (proof-string-match "Proof\\s-*\\(\\.\\|\\<with\\>\\)" str)))
+		)
+  )
+
 (defvar coq-keywords-kill-goal 
   '("Abort"))
 
@@ -725,7 +794,10 @@ Idtac (Nop) tactic, put the following line in your .emacs:
   (modify-syntax-entry ?_  "w")
   (modify-syntax-entry ?\' "_")
   (modify-syntax-entry ?\| ".")
-  (modify-syntax-entry ?\. "_")
+
+; should baybe be "_" but it makes coq-find-and-forget (in coq.el) bug
+  (modify-syntax-entry ?\. ".") 
+
   (condition-case nil
       ;; Try to use Emacs-21's nested comments.
       (modify-syntax-entry ?\* ". 23n")
@@ -735,5 +807,7 @@ Idtac (Nop) tactic, put the following line in your .emacs:
   (modify-syntax-entry ?\) ")(4"))
 
 
+
+
 (provide 'coq-syntax)
 ;;; coq-syntax.el ends here
diff --git a/coq/coq.el b/coq/coq.el
index 865eed8b..4bc20706 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -29,6 +29,7 @@
 ;; fix compilation
 
 (require 'coq-syntax)
+(require 'coq-indent)
 
 ;; Command to reset the Coq Proof Assistant
 ;; Pierre: added Impl... because of a bug of Coq until V6.3
@@ -331,70 +332,6 @@
   (proof-ids-to-regexp (append coq-keywords-decl coq-keywords-defn))
   "Declaration and definition regexp.")
 
-;; FIXME da: this one function breaks the nice configuration of Proof General:
-;; would like to have proof-goal-regexp instead.
-;; Unfortunately Coq allows "Definition" and friends to perhaps have a goal, 
-;; so it appears more difficult than just a proof-goal-regexp setting.
-;; Future improvement may simply to be allow a function value for
-;; proof-goal-regexp.
-
-;; excerpt of Jacek Chrzaszcz, implementer of the module system: sorry
-;; for the french:
-;*) suivant les suggestions de Chritine, pas de mode preuve dans un type de
-;    module (donc pas de Definition truc:machin.  Lemma, Theorem ... )
-;
-; *) la commande Module M [ ( : | <: ) MTYP ] [ := MEXPR ] est valable
-;    uniquement hors d'un MT
-;    - si :=MEXPR est absent, elle demarre un nouveau module interactif
-;    - si :=MEXPR est present, elle definit un module
-;    (la fonction vernac_define_module dans toplevel/vernacentries) 
-;
-; *) la nouvelle commande Declare Module M [ ( : | <: ) MTYP ] [ := MEXPR ]
-;    est valable uniquement dans un MT
-;    - si :=MEXPR absent, :MTYP absent, elle demarre un nouveau module
-;      interactif
-;    - si (:=MEXPR absent, :MTYP present) 
-;      ou (:=MEXPR present, :MTYP absent)
-;      elle declare un module.
-;    (la fonction vernac_declare_module dans toplevel/vernacentries)
-
-
-
-(defun coq-count-match (regexp strg)
-  "Count the number of (maximum, non overlapping) matching substring 
-of STRG matching REGEXP. Empty match are counted once."
-  (let ((nbmatch 0) (str strg))
-    (while (and (proof-string-match regexp str) (not (string-equal str "")))
-      (incf nbmatch)
-      (if (= (match-end 0) 0) (setq str (substring str 1))
-        (setq str (substring str (match-end 0)))))
-    nbmatch))
-
-
-
-(defun coq-goal-command-p (str)
-  "Decide whether argument is a goal or not"
-  (and (proof-string-match coq-goal-command-regexp str)
-       (not (proof-string-match "Local.*:=" str))
-       ;do not match Module t:T with Definition... 
-       (not (proof-string-match "\\`Definition.*:=" str))
-       (not (proof-string-match "\\`Module[^:]*:=" str))
-       ; Module ... (with Definition ..:=)* :=  --> module definition
-       ; Module ... (with Definition ..:=)*     --> module start
-       ; We count the number of
-       (not 
-        (and (proof-string-match "\\`Module[^:]*:\\(.*\\):=[^:]*" str)
-             (not (= (coq-count-match "\\<with\\>" str) (coq-count-match ":=" str)))))
-;       (not (proof-string-match module-with str))
-       (not (proof-string-match "Declare Module.*:" str)) ;neither : or :=
-       (not (proof-string-match "Recursive Definition" str))
-       ;; da: 3.4 test: do not exclude Lemma: we want goal-command-p to
-       ;; succeed for nested goals too now.
-       ;; (should we also exclude Definition?)
-       (not (proof-string-match "Lemma.*:=" str))))
-;; ))
-
-
 ; Pierre: This is a try, for use in find-and-forget. It seems to work but 
 ; is it correct with respect to the asynchronous communication between Coq 
 ; and emacs?  
@@ -812,15 +749,17 @@ This is specific to coq-mode."
 	proof-nested-undo-regexp coq-state-changing-commands-regexp)
   
   (setq	
-   proof-indent-close-offset -1
-   proof-indent-any-regexp
-   (proof-regexp-alt (proof-ids-to-regexp
-		      (append (list "Cases" "end") coq-keywords)) "\\s(" "\\s)")
-   proof-indent-enclose-regexp "|"
-   proof-indent-open-regexp
-   (proof-regexp-alt (proof-ids-to-regexp '("Cases")) "\\s(")
-   proof-indent-close-regexp
-   (proof-regexp-alt (proof-ids-to-regexp '("end")) "\\s)"))
+;indentation is implemented in coq-indent.el
+;   proof-indent-enclose-offset  (- proof-indent)
+;   proof-indent-enclose-offset 0
+;   proof-indent-close-offset 0
+;   proof-indent-open-offset 0
+   proof-indent-any-regexp      coq-indent-any-regexp
+;   proof-indent-inner-regexp    coq-indent-inner-regexp
+;   proof-indent-enclose-regexp  coq-indent-enclose-regexp
+   proof-indent-open-regexp     coq-indent-open-regexp
+   proof-indent-close-regexp    coq-indent-close-regexp
+)
 
 
   ;; span menu 
@@ -1075,9 +1014,6 @@ mouse activation."
 
 
 ;load the default coq abbrev file if no coq abbrev file is already read
-;TODO: add the holes and put holes in abbreviations.
-; This needs to add some code in generic/span*.el first, then add holes.el 
-; in the generaic part, and then ok.
 
 (if (and (boundp 'coq-mode-abbrev-table)
          (not (equal coq-mode-abbrev-table (make-abbrev-table))))
@@ -1088,6 +1024,7 @@ mouse activation."
   )
 
 
+
 (provide 'coq)
 
 
diff --git a/coq/ex-module.v b/coq/ex-module.v
index 227b3ff7..2fbdbcf5 100644
--- a/coq/ex-module.v
+++ b/coq/ex-module.v
@@ -1,22 +1,22 @@
 
 Module Type O1.
-Parameter A:Set.
-Parameter B:Set.
+  Parameter A:Set.
+  Parameter B:Set.
 End O1.
 
 
 Module R:O1.
-Definition A:=nat.
-Definition B:=bool.
+  Definition A:=nat.
+  Definition B:=bool.
 End R.
 
 Module R2: O1 with Definition  A:=nat.
-Definition A:=nat.
-Definition B:=bool.
+  Definition A:=nat.
+  Definition B:=bool.
 End R2.
 
 Module R4.
-Module R3: O1 with Definition  A:=nat :=R2.
+  Module R3: O1 with Definition  A:=nat :=R2.
 End R4.
 
 
@@ -28,8 +28,8 @@ Module M.
     Parameter x:T.
   End SIG.
   Lemma toto : O=O.
-  Definition t:=nat.
-	 Trivial.
+    Definition t:=nat.
+    Trivial.
   Save.
   Module N:SIG.
     Definition T:=nat.
@@ -43,54 +43,54 @@ Print t.
 
 
 Definition t:O=O.
-Trivial.
+  Trivial.
 Save.
 
 
 Section toto.
-Print M.
+  Print M.
 End toto.
 
 Module N:=M.
 
 
 Module Type typ.
-Parameter T:Set.
-Parameter a:T.
+  Parameter T:Set.
+  Parameter a:T.
 End typ.
 
 
 
 Module Type N'.
-Module Type M'.
-Declare Module K:N.SIG.
-End M'.
-Declare Module N''.
-  Definition T:=nat.
-  Definition x:=O.
-End N''.
-
-Declare Module N':M.SIG. (* no interactive def started *)
-Declare Module N''':= N'. (* no interactive def started *)
-Declare Module N''''. (* interactive def started *)
-Parameter foo:nat.
-End N''''.            (* interactive def ended *)
+  Module Type M'.
+    Declare Module K:N.SIG.
+  End M'.
+  Declare Module N''.
+    Definition T:=nat.
+    Definition x:=O.
+  End N''.
+
+  Declare Module N':M.SIG. (* no interactive def started *)
+  Declare Module N''':= N'. (* no interactive def started *)
+  Declare Module N''''. (* interactive def started *)
+    Parameter foo:nat.
+  End N''''.            (* interactive def ended *)
 End N'.
 
 
 
 Lemma titi : O=O.
-Trivial.
-Module Type K:=N'.
-Module N''':=M.
+  Trivial.
+  Module Type K:=N'.
+  Module N''':=M.
 Save.
 
 (* Here is a bug of Coq: *)
 
 Lemma bar:O=O.
-Module Type L. (* This should not be allowed by Coq, since the End L. below fails *)
-Axiom foo: O=O.
-End L. (* fails --> if we go back to Module Type: unsync *)
-Module I.
+  Module Type L. (* This should not be allowed by Coq, since the End L. below fails *)
+    Axiom foo: O=O.
+  End L. (* fails --> if we go back to Module Type: unsync *)
+  Module I.
 End I.