Clean whitespace

8 files changed, 114 insertions, 116 deletions

diff --git a/coq/coq-abbrev.el b/coq/coq-abbrev.el
index 7a24bf6c..a5131f10 100644
--- a/coq/coq-abbrev.el
+++ b/coq/coq-abbrev.el
@@ -1,5 +1,5 @@
 ;;; coq-abbrev.el --- coq abbrev table and menus for ProofGeneral mode
-;; Copyright (C) 1994 - 1998 LFCS Edinburgh. 
+;; Copyright (C) 1994 - 1998 LFCS Edinburgh.
 ;; Authors: Healfdene Goguen, Pierre Courtieu
 ;; License:     GPL (GNU GENERAL PUBLIC LICENSE)
 ;; Maintainer: Pierre Courtieu <Pierre.Courtieu@cnam.fr>
@@ -172,4 +172,3 @@
 
 
 (provide 'coq-abbrev)
-
diff --git a/coq/coq-autotest.el b/coq/coq-autotest.el
index 35e21030..ec5465e2 100644
--- a/coq/coq-autotest.el
+++ b/coq/coq-autotest.el
@@ -16,4 +16,3 @@
 
   (pg-autotest-quit-prover)
   (pg-autotest-finished))
-
diff --git a/coq/coq-db.el b/coq/coq-db.el
index bcc4a1e4..1be7719a 100644
--- a/coq/coq-db.el
+++ b/coq/coq-db.el
@@ -12,7 +12,7 @@
 ;;; real value defined below
 
 ;;; Commentary:
-;; 
+;;
 
 ;;; Code:
 
@@ -71,11 +71,11 @@ Insert corresponding string with holes at point.  If an insertion function is
 present for the keyword, call it instead.  see `coq-syntax-db' for DB
 structure."
   (let* ((tac (completing-read (concat prompt " (tab for completion) : ")
-                               db nil nil))
-         (infos (cddr (assoc tac db)))
-         (s (car infos)) ; completion to insert
-         (f (car-safe (cdr-safe (cdr-safe (cdr infos))))) ; insertion function
-         (pt (point)))
+			       db nil nil))
+	 (infos (cddr (assoc tac db)))
+	 (s (car infos)) ; completion to insert
+	 (f (car-safe (cdr-safe (cdr-safe (cdr infos))))) ; insertion function
+	 (pt (point)))
     (if f (funcall f) ; call f if present
       (insert (or s tac)) ; insert completion and indent otherwise
       (holes-replace-string-by-holes-backward-jump pt)
@@ -91,16 +91,16 @@ regexp.  See `coq-syntax-db' for DB structure."
   (let ((l db) (res ()))
     (while l
       (let* ((hd (car l)) (tl (cdr l))	; hd is the first infos list
-             (e1 (car hd)) (tl1 (cdr hd)) ; e1 = menu entry
-             (e2 (car tl1)) (tl2 (cdr tl1)) ; e2 = abbreviation
-             (e3 (car tl2)) (tl3 (cdr tl2)) ; e3 = completion
-             (e4 (car-safe tl3)) (tl4 (cdr-safe tl3)) ; e4 = state changing
-             (e5 (car-safe tl4)) (tl5 (cdr-safe tl4)) ; e5 = colorization string
-             )
-        ;; TODO delete doublons
-        (when (and e5 (or (not filter) (funcall filter hd)))
-          (setq res (nconc res (list e5)))) ; careful: nconc destructive!
-        (setq l tl)))
+	     (e1 (car hd)) (tl1 (cdr hd)) ; e1 = menu entry
+	     (e2 (car tl1)) (tl2 (cdr tl1)) ; e2 = abbreviation
+	     (e3 (car tl2)) (tl3 (cdr tl2)) ; e3 = completion
+	     (e4 (car-safe tl3)) (tl4 (cdr-safe tl3)) ; e4 = state changing
+	     (e5 (car-safe tl4)) (tl5 (cdr-safe tl4)) ; e5 = colorization string
+	     )
+	;; TODO delete doublons
+	(when (and e5 (or (not filter) (funcall filter hd)))
+	  (setq res (nconc res (list e5)))) ; careful: nconc destructive!
+	(setq l tl)))
     res
     ))
 
@@ -162,9 +162,9 @@ for DB structure."
 	  (car-safe (car-safe (nthcdr (- size 1) db)))))
 
 (defun coq-sort-menu-entries (menu)
-  (sort menu 
-	'(lambda (x y) (string< 
-			(downcase (elt x 0)) 
+  (sort menu
+	'(lambda (x y) (string<
+			(downcase (elt x 0))
 			(downcase (elt y 0))))))
 
 (defun coq-build-menu-from-db (db &optional size)
@@ -178,11 +178,11 @@ structure."
     (while l
       (if (<= lgth sz)
 	  (setq res ;; careful: nconc destructive!
-		(nconc res (list (cons 
+		(nconc res (list (cons
 				  (coq-build-title-menu l lgth)
 				  (coq-build-menu-from-db-internal l lgth wdth)))))
 	(setq res ; careful: nconc destructive!
-	      (nconc res (list (cons 
+	      (nconc res (list (cons
 				(coq-build-title-menu l sz)
 				(coq-build-menu-from-db-internal l sz wdth))))))
       (setq l (nthcdr sz l))
@@ -226,7 +226,7 @@ See `coq-syntax-db' for DB structure."
 
 
 ;;A new face for tactics which fail when they don't kill the current goal
-(defface coq-solve-tactics-face 
+(defface coq-solve-tactics-face
   (proof-face-specs
    (:foreground "red") ; pour les fonds clairs
    (:foreground "red") ; pour les fond foncés
diff --git a/coq/coq-indent.el b/coq/coq-indent.el
index d16b635a..bf506d7f 100644
--- a/coq/coq-indent.el
+++ b/coq/coq-indent.el
@@ -9,7 +9,7 @@
 
 
 ;;; Commentary:
-;; 
+;;
 
 (require 'coq-syntax)
 
@@ -73,7 +73,7 @@ detect if they start something or not."
          (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)
@@ -195,9 +195,9 @@ 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 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 
+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."
   ;; da: PATCH here for http://proofgeneral.inf.ed.ac.uk/trac/ticket/173
   ;; (nasty example).  But I don't understand this code!
@@ -312,7 +312,7 @@ not inside the {} of a record)."
     (let ((oldpt (point))
           (topnotreached (= (forward-line -1) 0))) ;;; nil if going one line backward
                                                    ;;; is not possible
-      
+
       (while (and topnotreached
                   (not (coq-find-no-syntactic-on-line))
                   t ;;(> (line-number (point)) (line-number (point-min)))
@@ -345,16 +345,16 @@ not inside the {} of a record)."
 
 (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 
+         (open-re  (if openreg
                        (proof-regexp-alt openreg proof-indent-open-regexp)
                      proof-indent-open-regexp))
-         (close-re (if closereg 
+         (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 
+         (nextpt (save-excursion
                    (proof-re-search-backward both-re))))
     (while
         (and (not (= lvl 0))
@@ -374,17 +374,17 @@ not inside the {} of a record)."
 
 
 (defun coq-find-at-same-level-zero (limit openreg)
-  "Move to open or openreg (first found) at same parenthesis level as point. 
+  "Move to open or openreg (first found) at same parenthesis level as point.
 Returns point if found."
   (let* ((found nil)
-         (open-re (if openreg 
+         (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 
+         (nextpt (save-excursion
                    (proof-re-search-backward both-re))))
-    
+
     (while
         (and (not found)
              (>= nextpt (or limit (point-min)))
@@ -403,7 +403,7 @@ Returns point if found."
 
 (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
@@ -421,10 +421,10 @@ Returns point if found."
       (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))))
 
@@ -466,13 +466,13 @@ Returns point if found."
         (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)
@@ -536,7 +536,7 @@ 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)))
-  
+
     (cond
 
      ;; at a ) -> same indent as the *line* of corresponding (
@@ -599,7 +599,7 @@ argument must be t if inside the {}s of a record, nil otherwise."
 ;;		(+ 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
@@ -611,10 +611,10 @@ argument must be t if inside the {}s of a record, nil otherwise."
      ((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 
+      (save-excursion
         (coq-find-unclosed 1 real-start)
         (back-to-indentation)
         (+ (current-column) proof-indent)))
@@ -623,7 +623,7 @@ argument must be t if inside the {}s of a record, nil otherwise."
      ((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)))
@@ -632,14 +632,14 @@ argument must be t if inside the {}s of a record, nil otherwise."
 
      ;; 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) 
+     ((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))))
 
 
@@ -666,7 +666,7 @@ argument must be t if inside the {}s of a record, nil otherwise."
          ((and (not atstart) (proof-looking-at-syntactic-context))
           (skip-chars-forward " \t")
           (current-column))
-         
+
             ;;we were at the first line of a comment and the current line is the
             ;;previous one
          (t (goto-char oldpt)
@@ -690,7 +690,7 @@ argument must be t if inside the {}s of a record, nil otherwise."
            (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) 
+	  ((= kind 3)
            (if notcomments nil (coq-indent-comment-offset))))))
 
 (defun coq-indent-calculate (&optional notcomments)
@@ -726,7 +726,7 @@ argument must be t if inside the {}s of a record, nil otherwise."
           (coq-indent-line-not-comments))
       (forward-line 1))
     (goto-char fin)))
- 
+
 
 ;;;   Local Variables: ***
 ;;;   fill-column: 85 ***
diff --git a/coq/coq-local-vars.el b/coq/coq-local-vars.el
index 0d7e5926..ed001679 100644
--- a/coq/coq-local-vars.el
+++ b/coq/coq-local-vars.el
@@ -7,11 +7,11 @@
 
 
 ;;; Commentary:
-;; 
+;;
 
 
 ;;; History:
-;; 
+;;
 
 ;;; Code:
 (defconst coq-local-vars-doc nil
diff --git a/coq/coq-mmm.el b/coq/coq-mmm.el
index 068543fb..21fa678e 100644
--- a/coq/coq-mmm.el
+++ b/coq/coq-mmm.el
@@ -5,7 +5,7 @@
 ;; Licence:	 GPL
 ;;
 ;; $Id$
-;; 
+;;
 ;; We only spot some simple cases of embedded LaTeX/HTML/verbatim.
 ;;
 ;; At the moment, the insertion has a bad interaction with the holes
diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el
index 00dbcf60..bc861f06 100644
--- a/coq/coq-syntax.el
+++ b/coq/coq-syntax.el
@@ -1,5 +1,5 @@
 ;; coq-syntax.el Font lock expressions for Coq
-;; Copyright (C) 1997-2007 LFCS Edinburgh. 
+;; Copyright (C) 1997-2007 LFCS Edinburgh.
 ;; Authors: Thomas Kleymann, Healfdene Goguen, Pierre Courtieu
 ;; License:     GPL (GNU GENERAL PUBLIC LICENSE)
 ;; Maintainer: Pierre Courtieu <Pierre.Courtieu@cnam.fr>
@@ -33,14 +33,14 @@
 ;; this one is temporary, for compatibility
 (defvar coq-version-is-V8 nil "Obsolete, use `coq-version-is-V8-0' instead.")
 
-(defvar coq-version-is-V8-0 nil 
+(defvar coq-version-is-V8-0 nil
   "This variable can be set to t to force ProofGeneral to coq version
  coq-8.0. To do that, put (setq coq-version-is-V8-0 t) in your .emacs and
  restart emacs. This variable cannot be true simultaneously with
  coq-version-is-V8-1. If none of these 2 variables is set to t, then
  ProofGeneral guesses the version of coq by doing 'coqtop -v'." )
 
-(defvar coq-version-is-V8-1 nil 
+(defvar coq-version-is-V8-1 nil
   "This variable can be set to t to force ProofGeneral to coq version
  coq-8.1 and above(use it for coq-8.0cvs after january 2005). To do
  that, put \(setq coq-version-is-V8-1 t) in your .emacs and restart
@@ -52,7 +52,7 @@
 (defun coq-determine-version ()
   "Intuit the version of Coq we're using and configure accordingly."
   ;; post-cond: one of the variables is set to t
-  (let* 
+  (let*
       (
        (seedoc (concat " (to force another version, see for example"
                        " C-h v `coq-version-is-V8-0)'."))
@@ -180,7 +180,7 @@
 
 
 (defvar coq-tactics-db
-  (append 
+  (append
    coq-user-tactics-db
    '(
      ("absurd " "abs" "absurd " t "absurd")
@@ -354,12 +354,12 @@
      ("solve" nil "solve [ # | # ]" nil "solve")
      ("tauto" "ta" "tauto" t "tauto")
      ))
-  "Coq tactic(al)s that solve a subgoal." 
+  "Coq tactic(al)s that solve a subgoal."
   )
 
 
 (defvar coq-tacticals-db
-  (append 
+  (append
    coq-user-tacticals-db
    '(
      ("info" nil "info #" nil "info")
@@ -398,7 +398,7 @@
     ("Parameters" "par" "Parameter #: #" t "Parameters")
     ("Conjecture" "conj" "Conjecture #: #." t "Conjecture")
     ("Variable" "v" "Variable #: #." t "Variable")
-    ("Variables" "vs" "Variables # , #: #." t "Variables")	
+    ("Variables" "vs" "Variables # , #: #." t "Variables")
     ("Coercion" "coerc" "Coercion @{id} : @{typ1} >-> @{typ2}." t "Coercion")
     )
   "Coq declaration keywords information list. See `coq-syntax-db' for syntax."
@@ -407,7 +407,7 @@
 (defvar coq-defn-db
   '(
     ("CoFixpoint" "cfix" "CoFixpoint # (#:#) : # :=\n#." t "CoFixpoint")
-    ("CoInductive" "coindv" "CoInductive # : # :=\n|# : #." t "CoInductive") 
+    ("CoInductive" "coindv" "CoInductive # : # :=\n|# : #." t "CoInductive")
     ("Declare Module : :=" "dm" "Declare Module # : # := #." t "Declare\\s-+Module")
     ("Declare Module <: :=" "dm2" "Declare Module # <: # := #." t);; careful
     ("Declare Module Import : :=" "dmi" "Declare Module # : # := #." t)
@@ -451,7 +451,7 @@
     ("Scheme" "sc" "Scheme @{name} := #." t "Scheme")
     ("Scheme Induction" "sci" "Scheme @{name} := Induction for # Sort #." t)
     ("Scheme Minimality" "scm" "Scheme @{name} := Minimality for # Sort #." t)
-    ("Structure" "str" "Structure # : # := {\n# : #;\n# : # }" t "Structure")	
+    ("Structure" "str" "Structure # : # := {\n# : #;\n# : # }" t "Structure")
     )
   "Coq definition keywords information list. See `coq-syntax-db' for syntax. "
   )
@@ -604,14 +604,14 @@
      ("Unset Printing Notations" "unsprn" "Unset Printing Notations" nil "Unset\\s-+Printing\\s-+Notations")
      ("Unset Undo" nil "Unset Undo." nil "Unset\\s-+Undo")
  ;    ("print" "pr" "print #" "print")
-     )   
+     )
    "Command that are not declarations, definition or goal starters."
   )
 
 (defvar coq-commands-db
   (append coq-decl-db coq-defn-db coq-goal-starters-db
           coq-other-commands-db coq-user-commands-db)
-  "Coq all commands keywords information list. See `coq-syntax-db' for syntax. "      
+  "Coq all commands keywords information list. See `coq-syntax-db' for syntax. "
   )
 
 
@@ -650,7 +650,7 @@
 
 ;; 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, 
+;; 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.
@@ -668,19 +668,19 @@
 ;;    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 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) 
+;;    - 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 
+  "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 "")))
@@ -706,12 +706,12 @@
 	 (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))
- 	 )
+	 (not				;
+	  (and
+	   (proof-string-match "\\`\\(Local\\|Definition\\|Lemma\\|Module\\)\\>" str)
+	   (not (= letwith affect))))
+	 (not (proof-string-match "\\`Declare\\s-+Module\\(\\w\\|\\s-\\|<\\)*:" str))
+	 )
     )
   )
 
@@ -722,14 +722,14 @@
 ;; TODO: have opened section/chapter in the prompt too, and get rid of
 ;; syntactical tests everywhere
 (defun coq-module-opening-p (str)
-  "Decide whether STR is a module or section opening or not. 
+  "Decide whether STR is a module or section opening or not.
 Used by `coq-goal-command-p'"
   (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)))
+	 (with (coq-count-match "\\<with\\>" str))
+	 (letwith (+ (coq-count-match "\\<let\\>" str) (- with match)))
+	 (affect (coq-count-match ":=" str)))
     (and (proof-string-match "\\`\\(Module\\)\\>" str)
- 	 (= letwith affect))
+	 (= letwith affect))
     ))
 
 (defun coq-section-command-p (str)
@@ -756,15 +756,15 @@ Used by `coq-goal-command-p'"
   (or (span-property span 'goalcmd)
       ;; module and section starts are detected here
       (let ((str (or (span-property span 'cmd) "")))
- 	(or (coq-section-command-p str)
- 	    (coq-module-opening-p str))
+	(or (coq-section-command-p str)
+	    (coq-module-opening-p str))
         )))
 
 ;; In coq > 8.1 This is used only for indentation.
 (defun coq-goal-command-str-p (str)
   "Decide whether argument is a goal or not.  Use
    `coq-goal-command-p' on a span instead if posible."
-  (cond 
+  (cond
    (coq-version-is-V8-1 (coq-goal-command-str-v81-p str))
    (coq-version-is-V8-0 (coq-goal-command-str-v80-p str))
    (t (coq-goal-command-str-v80-p str));; this is temporary
@@ -773,7 +773,7 @@ Used by `coq-goal-command-p'"
 ;; This is used for backtracking
 (defun coq-goal-command-p (span)
   "Decide whether argument is a goal or not."
-  (cond 
+  (cond
    (coq-version-is-V8-1 (coq-goal-command-p-v81 span))
    (coq-version-is-V8-0 (coq-goal-command-str-v80-p (span-property span 'cmd)))
    (t (coq-goal-command-str-v80-p (span-property span 'cmd)));; this is temporary
@@ -801,7 +801,7 @@ Used by `coq-goal-command-p'"
   )
 
 
-(defvar coq-keywords-kill-goal 
+(defvar coq-keywords-kill-goal
   '("Abort"))
 
 ;; Following regexps are all state changing
@@ -826,7 +826,7 @@ Used by `coq-goal-command-p'"
    coq-keywords-goal))                  ; idem
 
 
-;; 
+;;
 (defvar coq-keywords-state-preserving-commands
   (coq-build-regexp-list-from-db coq-commands-db 'filter-state-preserving))
 
@@ -834,7 +834,7 @@ Used by `coq-goal-command-p'"
 ;; whole commands-db
 (defvar coq-keywords-commands
   (append coq-keywords-state-changing-commands
- 	  coq-keywords-state-preserving-commands)
+	  coq-keywords-state-preserving-commands)
   "All commands keyword.")
 
 (defvar coq-solve-tactics
@@ -848,7 +848,7 @@ Used by `coq-goal-command-p'"
 
  ;; From JF Monin:
 (defvar coq-reserved
-  (append 
+  (append
    coq-user-reserved-db
    '(
      "False" "True" "after" "as" "cofix" "fix" "forall" "fun" "match"
@@ -877,7 +877,7 @@ Used by `coq-goal-command-p'"
 
 (defvar coq-keywords
   (append coq-keywords-goal coq-keywords-save coq-keywords-decl
- 	  coq-keywords-defn coq-keywords-commands)
+	  coq-keywords-defn coq-keywords-commands)
   "All keywords in a Coq script.")
 
 
@@ -910,7 +910,7 @@ Used by `coq-goal-command-p'"
 (defvar coq-ids (proof-ids coq-id " "))
 
 (defun coq-first-abstr-regexp (paren end)
-  (concat paren "\\s-*\\(" coq-ids "\\)\\s-*" end)) 
+  (concat paren "\\s-*\\(" coq-ids "\\)\\s-*" end))
 
 (defcustom coq-variable-highlight-enable t
   "Activates partial bound variable highlighting"
@@ -927,7 +927,7 @@ Used by `coq-goal-command-p'"
    (list (coq-first-abstr-regexp "\\<forall\\>" "\\(?:,\\|:\\)") 1 'font-lock-variable-name-face)
                                         ;   (list "\\<forall\\>"
                                         ;         (list 0 font-lock-type-face)
-                                        ;         (list (concat "[^ :]\\s-*\\(" coq-ids "\\)\\s-*") nil nil 
+                                        ;         (list (concat "[^ :]\\s-*\\(" coq-ids "\\)\\s-*") nil nil
                                         ;               (list 0 font-lock-variable-name-face)))
    ;; parenthesized binders
    (list (coq-first-abstr-regexp "(" ":[ a-zA-Z]") 1 'font-lock-variable-name-face)
@@ -940,27 +940,27 @@ Used by `coq-goal-command-p'"
 ;; It is understood here as being a goal.  This is important for
 ;; recognizing global identifiers, see coq-global-p.
 (defconst coq-save-command-regexp-strict
-  (proof-anchor-regexp 
+  (proof-anchor-regexp
    (concat "\\(Time\\s-+\\|\\)\\(" (proof-ids-to-regexp coq-keywords-save-strict)
            "\\)")))
 (defconst coq-save-command-regexp
-  (proof-anchor-regexp 
+  (proof-anchor-regexp
    (concat "\\(Time\\s-+\\|\\)\\(" (proof-ids-to-regexp coq-keywords-save)
            "\\)")))
 (defconst coq-save-with-hole-regexp
   (concat "\\(Time\\s-+\\|\\)\\(" (proof-ids-to-regexp coq-keywords-save-strict)
- 	  "\\)\\s-+\\(" coq-id "\\)\\s-*\\."))
+	  "\\)\\s-+\\(" coq-id "\\)\\s-*\\."))
 
 (defconst coq-goal-command-regexp
   (proof-anchor-regexp (proof-ids-to-regexp coq-keywords-goal)))
 
 (defconst coq-goal-with-hole-regexp
   (concat "\\(" (proof-ids-to-regexp coq-keywords-goal)
- 	  "\\)\\s-+\\(" coq-id "\\)\\s-*:?"))
+	  "\\)\\s-+\\(" coq-id "\\)\\s-*:?"))
 
 (defconst coq-decl-with-hole-regexp
   (concat "\\(" (proof-ids-to-regexp coq-keywords-decl)
- 	  "\\)\\s-+\\(" coq-ids "\\)\\s-*:"))
+	  "\\)\\s-+\\(" coq-ids "\\)\\s-*:"))
 
 ;;  (defconst coq-decl-with-hole-regexp
 ;;    (if coq-variable-highlight-enable coq-decl-with-hole-regexp-1 'nil))
@@ -973,10 +973,10 @@ Used by `coq-goal-command-p'"
 ;; "with f x y :" (followed by = or not)
 ;; "with f x y (z:" (not followed by =)
 ;; BUT NOT:
-;; "with f ... (x:=" 
+;; "with f ... (x:="
 ;; "match ... with .. => "
 (defconst coq-with-with-hole-regexp
-  (concat "\\(with\\)\\s-+\\(" coq-id "\\)\\s-*\\([^=(.]*:\\|[^(]*(\\s-*" 
+  (concat "\\(with\\)\\s-+\\(" coq-id "\\)\\s-*\\([^=(.]*:\\|[^(]*(\\s-*"
           coq-id "\\s-*:[^=]\\)"))
 ;; marche aussi a peu pres
 ;;  (concat "\\(with\\)\\s-+\\(" coq-id "\\)\\s-*\\([^(.]*:\\|.*)[^(.]*:=\\)"))
@@ -999,7 +999,7 @@ Used by `coq-goal-command-p'"
           (list 1 'font-lock-function-name-face t))
 
     (list coq-goal-with-hole-regexp 2 'font-lock-function-name-face))
-    (if coq-variable-highlight-enable 
+    (if coq-variable-highlight-enable
         (list (list coq-decl-with-hole-regexp 2 'font-lock-variable-name-face)))
     (list
     (list coq-defn-with-hole-regexp 2 'font-lock-function-name-face)
@@ -1028,7 +1028,7 @@ Used by `coq-goal-command-p'"
   (modify-syntax-entry ?\| ".")
 
 ;; should maybe be "_" but it makes coq-find-and-forget (in coq.el) bug
-  (modify-syntax-entry ?\. ".") 
+  (modify-syntax-entry ?\. ".")
 
   (condition-case nil
       ;; Try to use Emacs-21's nested comments.
@@ -1040,11 +1040,11 @@ Used by `coq-goal-command-p'"
 
 
 (defconst coq-generic-expression
-  (mapcar (lambda (kw) 
- 	    (list (capitalize kw)
- 		  (concat "\\<" kw "\\>" "\\s-+\\(\\w+\\)\\W" )
- 		  1))
- 	  (append coq-keywords-decl coq-keywords-defn coq-keywords-goal)))
+  (mapcar (lambda (kw)
+	    (list (capitalize kw)
+		  (concat "\\<" kw "\\>" "\\s-+\\(\\w+\\)\\W" )
+		  1))
+	  (append coq-keywords-decl coq-keywords-defn coq-keywords-goal)))
 
 (provide 'coq-syntax)
  ;;; coq-syntax.el ends here
diff --git a/coq/coq-unicode-tokens.el b/coq/coq-unicode-tokens.el
index b7a0692a..84beb4b6 100644
--- a/coq/coq-unicode-tokens.el
+++ b/coq/coq-unicode-tokens.el
@@ -161,7 +161,7 @@ You can adjust this table to add more entries, or to change entries for
 glyphs that not are available in your Emacs or chosen font.
 
 These shortcuts are only used for input; no reverse conversion is
-performed.  This means that the target strings need to have a defined 
+performed.  This means that the target strings need to have a defined
 meaning to be useful."
   :type '(repeat (cons (string :tag "Shortcut sequence")
 		       (string :tag "Unicode string")))
@@ -169,24 +169,24 @@ meaning to be useful."
   :group 'coq
   :tag "Coq Unicode Input Shortcuts")
 
-  
+
 ;;
 ;; Controls
 ;;
 
-(defconst coq-control-char-format-regexp 
+(defconst coq-control-char-format-regexp
   ;; FIXME: fix Coq identifier syntax below
   "\\(\s*%s\s*\\)\\([a-zA-Z0-9']+\\)")
 
 (defconst coq-control-char-format " %s ")
 
-(defconst coq-control-characters 
-  '(("Subscript" "__" sub) 
+(defconst coq-control-characters
+  '(("Subscript" "__" sub)
     ("Superscript" "^^" sup)))
 
 (defconst coq-control-region-format-regexp "\\(\s*%s\{\\)\\([^}]*\\)\\(\}\s*\\)")
 
-(defconst coq-control-regions 
+(defconst coq-control-regions
   '(("Subscript" "," "" sub)
     ("Superscript" "^" "" sup)
     ("Bold" "BOLD" "" bold)