replace-in-string-> replace-regexp-in-string

1 files changed, 129 insertions, 129 deletions

diff --git a/coq/coq.el b/coq/coq.el
index a7048ced..4b9db823 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -4,7 +4,7 @@
 ;; License:     GPL (GNU GENERAL PUBLIC LICENSE)
 ;; Maintainer: Pierre Courtieu <Pierre.Courtieu@cnam.fr>
 
-;; $Id$ 
+;; $Id$
 
 
 ;;; Commentary:
@@ -51,14 +51,14 @@
 (defun coq-build-prog-args ()
   (setq coq-prog-args
         (append (remove-if (lambda (x) (string-match "\\-emacs" x)) coq-prog-args)
-                (cond 
+                (cond
                  (coq-version-is-V8-0 '("-emacs"))
                  (t '("-emacs-U")))
                 (if coq-translate-to-v8 " -translate")))
   )
 
 ;; fix it
-(unless noninteractive ;; compiling 
+(unless noninteractive ;; compiling
   (coq-build-prog-args))
 
 (defcustom coq-compile-file-command "coqc %s"
@@ -82,7 +82,7 @@ Set to t if you want this feature."
   :type 'number
   :group 'coq)
 
-(defconst coq-shell-init-cmd 
+(defconst coq-shell-init-cmd
   (format "Set Undo %s . " coq-default-undo-limit))
 
 ;; da 15/02/03: moved setting of coq-version-is-vX to coq-syntax to
@@ -91,7 +91,7 @@ Set to t if you want this feature."
 (require 'coq-syntax)
 (require 'coq-indent)
 
-(if coq-version-is-V8-0 
+(if coq-version-is-V8-0
     (setq proof-shell-unicode nil))
 
 (defcustom coq-prog-env nil
@@ -99,18 +99,18 @@ Set to t if you want this feature."
 On Windows you might need something like:
   (setq coq-prog-env '(\"HOME=C:\\Program Files\\Coq\\\"))"
   :group 'coq)
-  
+
 
 ;; Command to reset the Coq Proof Assistant
 (defconst coq-shell-restart-cmd "Reset Initial.\n ")
 
 
-;; NB: da: PG 3.5: added \n here to account for blank line in Coq output. 
+;; NB: da: PG 3.5: added \n here to account for blank line in Coq output.
 ;; Better result for shrinking windows, grabbing shell output.
-;; Pierre added the infos in the prompt, this is new in Coq v8-1 
+;; Pierre added the infos in the prompt, this is new in Coq v8-1
 
-(defvar coq-shell-prompt-pattern 
-  (if coq-version-is-V8-1 
+(defvar coq-shell-prompt-pattern
+  (if coq-version-is-V8-1
       (concat "\\(?:\n\\(?:[^\n\371]+\371\\|<prompt>[^\n]+</prompt>\\)\\)")
     (concat "\\(?:\n" proof-id " < \371\\)"))
     "*The prompt pattern for the inferior shell running coq.")
@@ -136,7 +136,7 @@ On Windows you might need something like:
 
 ;; Configuration
 
-(defun coq-library-directory () 
+(defun coq-library-directory ()
   (let ((c (substring (shell-command-to-string "coqtop -where") 0 -1 )))
     (if (string-match c "not found")
 	  "/usr/local/lib/coq"
@@ -164,8 +164,8 @@ On Windows you might need something like:
 ;; ----- outline
 ;; FIXME, deal with interacive "Definition"
 (defvar coq-outline-regexp
-;;  (concat "(\\*\\|" 
-  (concat "[ ]*" (regexp-opt 
+;;  (concat "(\\*\\|"
+  (concat "[ ]*" (regexp-opt
 	   '(
              "Ltac" "Corr" "Modu" "Sect" "Chap" "Goal" "Definition" "Lemm" "Theo" "Fact" "Rema" "Mutu" "Fixp" "Func") t)))
 ;)
@@ -184,24 +184,24 @@ On Windows you might need something like:
 
 ;; some of them must kept when v8.1 because they are used by state preserving
 ;; check when C-c C-v
-(defconst coq-state-preserving-tactics-regexp 
+(defconst coq-state-preserving-tactics-regexp
   (proof-ids-to-regexp coq-state-preserving-tactics))
 (defconst coq-state-changing-commands-regexp
   (proof-ids-to-regexp coq-keywords-state-changing-commands))
-(defconst coq-state-preserving-commands-regexp 
+(defconst coq-state-preserving-commands-regexp
   (proof-ids-to-regexp coq-keywords-state-preserving-commands))
-(defconst coq-commands-regexp 
+(defconst coq-commands-regexp
   (proof-ids-to-regexp coq-keywords-commands))
-(defvar coq-retractable-instruct-regexp 
+(defvar coq-retractable-instruct-regexp
   (proof-ids-to-regexp coq-retractable-instruct))
-(defvar coq-non-retractable-instruct-regexp 
+(defvar coq-non-retractable-instruct-regexp
   (proof-ids-to-regexp coq-non-retractable-instruct))
 
 ; delete when no more support for 8.0 ?
 (defvar coq-keywords-section
   '("Section" "Module\\s-+Type" "Declare\\s-+Module" "Module"))
 
-(defvar coq-section-regexp 
+(defvar coq-section-regexp
   (concat "\\(" (proof-ids-to-regexp coq-keywords-section) "\\)")
 ;  "\\(\\<Section\\>\\|\\<Module\\>\\s-+\\<Type\\>\\|\\<Module\\>\\)"
 )
@@ -211,12 +211,12 @@ On Windows you might need something like:
 ;;   Derived modes - they're here 'cos they define keymaps 'n stuff ;;
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
-(eval-and-compile 
+(eval-and-compile
   (define-derived-mode coq-shell-mode proof-shell-mode
     "coq-shell" nil
     (coq-shell-mode-config)))
-  
-(eval-and-compile 
+
+(eval-and-compile
   (define-derived-mode coq-response-mode proof-response-mode
   "CoqResp" nil
     (coq-response-config)))
@@ -244,7 +244,7 @@ On Windows you might need something like:
 ;; da: have now combined count-undos and find-and-forget, they're the
 ;; same now we deal with nested proofs and send general sequence
 ;; "Abort. ... Abort. BackTo n. Undo n."
-;; pc: now we do even better: "Backtrack n m p. " based on infos in 
+;; pc: now we do even better: "Backtrack n m p. " based on infos in
 ;; the prompt.
 
 ;; All this is to be removed when coq > 8.0 (until the "End remove" below)
@@ -254,7 +254,7 @@ On Windows you might need something like:
   "Declaration and definition regexp.")
 
 (defun coq-proof-mode-p ()
-  "Return true if we are currentlly in proof mode. 
+  "Return true if we are currentlly in proof mode.
 Look at the last line of the *coq* buffer to see if the prompt is the
 toplevel \"Coq <\".  Returns nil if yes.  This assumes that no
 \"Resume\" or \"Suspend\" command has been used."
@@ -264,17 +264,17 @@ toplevel \"Coq <\".  Returns nil if yes.  This assumes that no
 ;; DA: rewrote to combine behaviour with count-undos, to work with
 ;; nested proofs.
 
-(defun coq-is-comment-or-proverprocp (span) 
+(defun coq-is-comment-or-proverprocp (span)
   (memq (span-property span 'type) '(comment proverproc)))
 (defun coq-is-goalsave-p (span) (eq (span-property span 'type) 'goalsave))
 (defun coq-is-module-equal-p (str) ;;cannot appear vith coq < 7.4
   (and (proof-string-match "\\`\\(Declare\\s-\\)?\\s-*\\<Module\\>.*:=" str)
        (not (proof-string-match "\\<with\\>" str))))
-(defun coq-is-def-p (str) 
+(defun coq-is-def-p (str)
   (proof-string-match (concat "\\`Definition\\s-+\\(" proof-id "\\)\\s-*") str))
 (defun coq-is-decl-defn-p (str)
-  (proof-string-match 
-   (concat "\\`\\(" coq-keywords-decl-defn-regexp "\\)\\s-*\\(" 
+  (proof-string-match
+   (concat "\\`\\(" coq-keywords-decl-defn-regexp "\\)\\s-*\\("
            proof-id "\\)\\s-*[\\[,:.]") str))
 
 (defun coq-state-preserving-command-p (str)
@@ -284,13 +284,13 @@ toplevel \"Coq <\".  Returns nil if yes.  This assumes that no
   (proof-string-match (concat "\\`\\(" coq-commands-regexp "\\)") str))
 
 (defun coq-state-preserving-tactic-p (str)
-  (proof-string-match 
-   (concat "\\`\\(" 
+  (proof-string-match
+   (concat "\\`\\("
            coq-state-preserving-tactics-regexp "\\)") str))
 
 (defun coq-state-changing-tactic-p (str) ; unknown things are considered (state
                                         ;changing) tactics here
-  (and (not (coq-command-p str)) 
+  (and (not (coq-command-p str))
        (not (coq-state-preserving-tactic-p str)))
   )
 
@@ -299,13 +299,13 @@ toplevel \"Coq <\".  Returns nil if yes.  This assumes that no
   (proof-string-match (concat "\\`\\(" coq-state-changing-commands-regexp "\\)") str))
 
 ; if no second id --> name of the module/section is (match-string 2 str)
-; otherwise it is (match-string 5 str) 
+; otherwise it is (match-string 5 str)
 ; to know if there is a second id: (match-string 2 str)="Type" ?
 ; delete when no more support for 8.0
 (defun coq-section-or-module-start-p (str)
-  (proof-string-match 
-   (concat "\\`" coq-section-regexp 
-           "\\s-+\\(" proof-id "\\)\\(\\s-*\\(" proof-id "\\)\\)?") str)) 
+  (proof-string-match
+   (concat "\\`" coq-section-regexp
+           "\\s-+\\(" proof-id "\\)\\(\\s-*\\(" proof-id "\\)\\)?") str))
 
 ;; End of remove when coq > 8.0
 
@@ -327,7 +327,7 @@ toplevel \"Coq <\".  Returns nil if yes.  This assumes that no
 (defun coq-last-prompt-info (s)
   "Extract informations from the coq prompt S.  See `coq-last-prompt-info-safe'."
   (let ((lastprompt (or s (error "no prompt !!?")))
-        (regex 
+        (regex
          (concat "\\(" coq-id-shy "\\) < \\([0-9]+\\) |\\(\\(?:" coq-id-shy
                  "|?\\)*\\)| \\([0-9]+\\) < ")))
     (when (string-match regex lastprompt)
@@ -344,7 +344,7 @@ pending proofs (in a list)."
 
 (defvar coq-last-but-one-statenum 1
   "The state number we want to put in a span.
-This is the prompt number given *just before* the command was sent. 
+This is the prompt number given *just before* the command was sent.
 This variable remembers this number and will be updated when
 used see coq-set-state-number. Initially 1 because Coq initial state has number 1.")
 
@@ -394,7 +394,7 @@ used see coq-set-state-number. Initially 1 because Coq initial state has number
   (span-set-property span 'proofstack val)
   )
 
-(defun proof-last-locked-span () 
+(defun proof-last-locked-span ()
   (save-excursion ;; didn't found a way to avoid buffer switching
     (set-buffer proof-script-buffer)
     (span-at (- (proof-locked-end) 1) 'type)
@@ -423,9 +423,9 @@ If locked span already has a state number, thne do nothing. Also updates
         (unless (or (not sp) (coq-get-span-statenum sp))
           (coq-set-span-statenum sp coq-last-but-one-statenum))
         (setq coq-last-but-one-statenum (car infos))
-        ;; set goalcmd property if this is a goal start 
+        ;; set goalcmd property if this is a goal start
         ;; (ie proofstack has changed and not a save cmd)
-        (unless 
+        (unless
             (or (not sp) (equal (span-property sp 'type) 'goalsave)
                 (<= (length (car (cdr (cdr infos))))
                     (length coq-last-but-one-proofstack)))
@@ -443,15 +443,15 @@ If locked span already has a state number, thne do nothing. Also updates
     )
   )
 
-;; This hook seems the one we want (if we are in V8.1 mode only).  
+;; This hook seems the one we want (if we are in V8.1 mode only).
 ;; WARNING! It is applied once after each command PLUS once before a group of
 ;; commands is started
-(add-hook 'proof-state-change-hook 
+(add-hook 'proof-state-change-hook
           '(lambda () (if coq-version-is-V8-1 (coq-set-state-infos))))
 
 (defun count-not-intersection (l notin)
   "Return the number of elts of L that are not in NOTIN."
-  
+
   (let ((l1 l) (l2 notin) (res 0))
     (while l1
       (if (member (car l1) l2) ()
@@ -468,12 +468,12 @@ If locked span already has a state number, thne do nothing. Also updates
 ;;       __                              _
 ;; aux < 12 |aux|SmallStepAntiReflexive| 4 < ù
 ;; ^^^^^^   ^^^^^^^^^^^^^^^^^^^^^^^^^^^^     ^
-;; usual           pending proofs           usual 
+;; usual           pending proofs           usual
 ;;                                          special char
 ;; exemple:
 ;; to go (back) from 12 |lema1|lema2...|leman| xx
 ;; to                8  |lemb1|lemb2...|lembm| 5
-;; we must do "Backtrack 8 5 naborts" 
+;; we must do "Backtrack 8 5 naborts"
 ;; where naborts is the number of lemais that are not lembis
 
 ;; Rem: We could deal with suspend and resume with more work. We would need a new coq
@@ -494,7 +494,7 @@ If locked span already has a state number, thne do nothing. Also updates
                (= coq-last-but-one-proofnum proofdepth)
                (= coq-last-but-one-statenum span-staten))
               ""
-            (format "Backtrack %s %s %s . " 
+            (format "Backtrack %s %s %s . "
                     (int-to-string span-staten)
                     (int-to-string proofdepth)
                     naborts)))
@@ -515,7 +515,7 @@ If locked span already has a state number, thne do nothing. Also updates
       (cond
        ((coq-is-comment-or-proverprocp span)) ; do nothing
 
-       ;; Module <Type> T ... :=... . inside proof ->  like Definition...:=...  
+       ;; Module <Type> T ... :=... . inside proof ->  like Definition...:=...
        ;; (should actually be disallowed in coq)
        ; Should go in last cond, but I have a problem trying to avoid next cond to match.
        ((and (coq-proof-mode-p) (coq-is-module-equal-p str)) (incf nbacks))
@@ -538,10 +538,10 @@ If locked span already has a state number, thne do nothing. Also updates
         ;; da: try using just Back since "Reset" causes loss of proof state.
         (if (span-property span 'nestedundos)
             ;; Pierre: more robust when some unknown commands are not well backtracked
-            (if (and (= (span-property span 'nestedundos) 0) (not (coq-proof-mode-p))) 
+            (if (and (= (span-property span 'nestedundos) 0) (not (coq-proof-mode-p)))
                 (setq ans (format coq-forget-id-command (span-property span 'name)))
               (setq nbacks (+ 1 nbacks (span-property span 'nestedundos))))))
-       
+
        ;; Unsaved goal commands: each time we hit one of these
        ;; we need to issue Abort to drop the proof state.
        ((coq-goal-command-str-p str) (incf naborts)) ; FIX: nundos<-0 ?
@@ -550,12 +550,12 @@ If locked span already has a state number, thne do nothing. Also updates
        ;; to see if the undoing will take us outside a proof, and use the first Reset
        ;; found if so: but this is tricky to co-ordinate with the number of Backs,
        ;; perhaps? ]
-       ((and (not (coq-proof-mode-p));; (eq proof-nesting-depth 0) 
+       ((and (not (coq-proof-mode-p));; (eq proof-nesting-depth 0)
              (coq-is-decl-defn-p str))
         (setq ans (format coq-forget-id-command (match-string 2 str))))
-		 
-       ;; Outside a proof: cannot be a tactic, if unknown: do back 
-       ;; (we may decide otherwise, it is false anyhow, use elisp 
+
+       ;; Outside a proof: cannot be a tactic, if unknown: do back
+       ;; (we may decide otherwise, it is false anyhow, use elisp
        ;; vars instead for the perfect thing).
        ((and (not (coq-proof-mode-p)) (not (coq-state-preserving-command-p str)))
         (incf nbacks))
@@ -565,7 +565,7 @@ If locked span already has a state number, thne do nothing. Also updates
        ;; tactics are considered needing undo, use elisp vars for the 1% remaining).
        ;; no undo if abort
        ((coq-proof-mode-p)
-        (cond 
+        (cond
          ((coq-state-changing-command-p str) (incf nbacks))
          ((and (eq 0 naborts)
                (not (coq-state-preserving-command-p str))
@@ -589,10 +589,10 @@ If locked span already has a state number, thne do nothing. Also updates
                  aborts))
            (if (> nbacks 0)
                (concat "Back " (int-to-string nbacks) ". "))
-           (if (> nundos 0) 
+           (if (> nundos 0)
                (concat "Undo " (int-to-string nundos) ". "))))
 
-    (if (null ans) nil;; [was proof-no-command] FIXME: this is an error really (assert nil); 
+    (if (null ans) nil;; [was proof-no-command] FIXME: this is an error really (assert nil);
       (if (string-equal ans "") nil ;; [was proof-no-command] ; not here because if
 						 ; we backtrack a state preserving command, we must do
 						 ; *nothing*, not even a CR (in v74, no prompt is returned
@@ -609,18 +609,18 @@ This function calls `coq-find-and-forget-v81' or `coq-find-and-forget-v80'
 depending on the variables `coq-version-is-V8-1' and `coq-version-is-V8-0', if
 none is set, then it default to `coq-find-and-forget-v81' but this should not
 happen since one of them is necessarily set to t in coq-syntax.el."
- (cond 
+ (cond
   (coq-version-is-V8-1 (coq-find-and-forget-v81 span))
   (coq-version-is-V8-0 (coq-find-and-forget-v80 span))
   (t (coq-find-and-forget-v81 span)) ;; should not happen
   )
- )  
+ )
 
 (defvar coq-current-goal 1
   "Last goal that Emacs looked at.")
 
 (defun coq-goal-hyp ()
-  (cond 
+  (cond
    ((looking-at "============================\n")
     (goto-char (match-end 0))
     (cons 'goal (int-to-string coq-current-goal)))
@@ -633,11 +633,11 @@ happen since one of them is necessarily set to t in coq-syntax.el."
    (t nil)))
 
 (defun coq-state-preserving-p (cmd)
-;  (or 
-   (proof-string-match coq-non-retractable-instruct-regexp cmd)) 
-;   (and 
+;  (or
+   (proof-string-match coq-non-retractable-instruct-regexp cmd))
+;   (and
 ;    (not (proof-string-match coq-retractable-instruct-regexp cmd))
-;    (or 
+;    (or
 ;     (message "Unknown command, hopes this won't desynchronize ProofGeneral")
 ;     t))))
 
@@ -646,23 +646,23 @@ happen since one of them is necessarily set to t in coq-syntax.el."
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
 
-(defconst notation-print-kinds-table 
+(defconst notation-print-kinds-table
   '(("Print Scope(s)" 0) ("Print Visibility" 1))
   "Enumerates the different kinds of notation information one can ask to coq.")
 
 (defun coq-PrintScope ()
   "Show information on notations. Coq specific."
   (interactive)
-  (let* 
-      ((mods 
-        (completing-read "Infos on notation (tab to see list): " 
+  (let*
+      ((mods
+        (completing-read "Infos on notation (tab to see list): "
                          notation-print-kinds-table))
        (s (read-string  "Name (empty for all): "))
        (all (string-equal s "")))
-    (cond 
-     ((and (string-equal mods "Print Scope(s)") (string-equal s "")) 
+    (cond
+     ((and (string-equal mods "Print Scope(s)") (string-equal s ""))
       (proof-shell-invisible-command (format "Print Scopes.")))
-     (t 
+     (t
       (proof-shell-invisible-command (format "%s %s ." mods s)))
      )
     )
@@ -685,10 +685,10 @@ happen since one of them is necessarily set to t in coq-syntax.el."
 (defun coq-ask-do (ask do &optional dontguess postformatcmd)
   "Ask for an ident and print the corresponding term."
   (let* ((cmd) (postform (if (eq postformatcmd nil) 'identity postformatcmd)))
-    (proof-shell-ready-prover) 
+    (proof-shell-ready-prover)
     (setq cmd (coq-guess-or-ask-for-string ask dontguess))
     (proof-shell-invisible-command
-     (format (concat do " %s . ") (funcall postform cmd))))  
+     (format (concat do " %s . ") (funcall postform cmd))))
   )
 
 (defun coq-SearchIsos ()
@@ -735,7 +735,7 @@ This is specific to `coq-mode'."
   "Locate a notation.
 This is specific to `coq-mode'."
   (interactive)
-  (coq-ask-do "Locate Notation (ex: \'exists\' _ , _)" "Locate" 
+  (coq-ask-do "Locate Notation (ex: \'exists\' _ , _)" "Locate"
               t 'coq-addquotes))
 
 (defun coq-Pwd ()
@@ -792,7 +792,7 @@ This is specific to `coq-mode'."
 
 (defun coq-guess-command-line (filename)
   "Guess the right command line options to compile FILENAME using `make -n'."
-  (if (local-variable-p 'coq-prog-name (current-buffer)) 
+  (if (local-variable-p 'coq-prog-name (current-buffer))
       coq-prog-name
     (let* ((dir (or (file-name-directory filename) "."))
            (makedir
@@ -845,7 +845,7 @@ This is specific to `coq-mode'."
   ;; Coq error messages are thrown off by TAB chars.
   (set (make-local-variable 'indent-tabs-mode) nil)
   (setq proof-terminal-char ?\.)
-  (setq proof-script-command-end-regexp 
+  (setq proof-script-command-end-regexp
         "\\(?:[^.]\\|\\(?:\\.\\.\\)\\)\\.\\(\\s-\\|\\'\\)")
   (setq proof-script-comment-start "(*")
   (setq proof-script-comment-end "*)")
@@ -884,8 +884,8 @@ This is specific to `coq-mode'."
 	proof-nested-undo-regexp coq-state-changing-commands-regexp
   proof-script-imenu-generic-expression coq-generic-expression
   )
-  
-  (setq	
+
+  (setq
    indent-line-function 'coq-indent-line
 ;indentation is implemented in coq-indent.el
 ;   proof-indent-enclose-offset  (- proof-indent)
@@ -903,7 +903,7 @@ This is specific to `coq-mode'."
   (setq indent-region-function 'coq-indent-region)
 
 
-  ;; span menu 
+  ;; span menu
   (setq proof-script-span-context-menu-extensions 'coq-create-span-menu)
 
   (setq proof-shell-start-silent-cmd "Set Silent. "
@@ -945,28 +945,28 @@ This is specific to `coq-mode'."
   ;; now lost in define-derived-mode for some reason.
   (add-hook 'proof-activate-scripting-hook 'proof-cd-sync nil t)
   (add-hook 'proof-deactivate-scripting-hook 'coq-maybe-compile-buffer nil t))
-  
+
 
 (defvar coq-last-hybrid-pre-string "")
 ;; pc: TODO: Have a generic way to split one output into several outputs
 ;; Actually this could be done by adapting process-delayed-output.
 (defun coq-hybrid-ouput-goals-response-p (cmd string)
-  "Specific test function to detect hybrid response/goal output from coq. 
+  "Specific test function to detect hybrid response/goal output from coq.
 To be used in `proof-shell-classify-output-system-specific'. "
-  (proof-shell-string-match-safe "[0-9]+ subgoals?" string)  
+  (proof-string-match-safe "[0-9]+ subgoals?" string)
   )
 
 (defun coq-hybrid-ouput-goals-response (cmd string)
-  "Specific function to deal with hybrid response/goal output from coq. 
+  "Specific function to deal with hybrid response/goal output from coq.
 To be used in `proof-shell-classify-output-system-specific'."
   ;; match subgoal list anywhere in the ouput
   ;; then display the message before it, and then do as a normal goal
   ;; output.
-  (proof-shell-string-match-safe "[0-9]+ subgoals?" string) 
+  (proof-shell-string-match-safe "[0-9]+ subgoals?" string)
   (let* ((start (match-beginning 0))
          (prestring (substring string 0 start))
          (goalstring (substring string start)))
-    (unless nil ;(not (null proof-action-list)) 
+    (unless nil ;(not (null proof-action-list))
       ;(setq proof-shell-last-output goalstring)
       ;(setq proof-shell-last-output-kind 'goals)
       ;; (proof-shell-classify-output cmd goalstring)
@@ -978,7 +978,7 @@ To be used in `proof-shell-classify-output-system-specific'."
 
 
 (defun coq-shell-mode-config ()
-  (setq 
+  (setq
    proof-shell-cd-cmd coq-shell-cd
    proof-shell-filename-escapes '(("\\\\" . "\\\\") ("\""   . "\\\""))
    proof-shell-abort-goal-regexp coq-shell-abort-goal-regexp
@@ -1013,7 +1013,7 @@ To be used in `proof-shell-classify-output-system-specific'."
    proof-shell-classify-output-system-specific
    '(coq-hybrid-ouput-goals-response-p . coq-hybrid-ouput-goals-response)
    )
-  
+
   (coq-init-syntax-table)
   ; da: suggest no fontification in shell
   ;(setq font-lock-defaults 'coq-font-lock-keywords-1)
@@ -1118,11 +1118,11 @@ To be used in `proof-shell-classify-output-system-specific'."
 ;;
 ;; This is an imperfect attempt.  It really needs prover assistance.
 ;;
-;; Experimental support for multiple files was first added 
+;; Experimental support for multiple files was first added
 ;; for Coq 6.X based on discussions at TYPES 2000 between DA and PC.
 ;; Updated and simplified for Coq 8, PG 3.5 (22.04.04) by DA.
 
-;; First note that coq-shell-cd is sent whenever we activate scripting, 
+;; First note that coq-shell-cd is sent whenever we activate scripting,
 ;; it extends the loadpath with the current directory.
 
 ;; When scripting is turned off, we compile the file to update the .vo.
@@ -1137,14 +1137,14 @@ This is a value for the `proof-deactivate-scripting-hook'."
         ;; FIXME: in PG 4, this next step will be done inside
         ;; proof-register-possibly-new-processed-file.
         ;; NB: we might save dependent buffers too!
-        (ignore-errors 
+        (ignore-errors
           (proof-save-some-buffers (list buffer)))
         ;; Now re-compile.
         ;; Coq users like Make, let's see if we have a Makefile
         ;; here and choose compile.
         (cond
-         ((and (proof-try-require 'compile) 
-               compile-command 
+         ((and (proof-try-require 'compile)
+               compile-command
                (file-exists-p "Makefile"))
           ;; NB: compilation is run in the background
           ;; in this case!
@@ -1152,7 +1152,7 @@ This is a value for the `proof-deactivate-scripting-hook'."
             (call-interactively 'compile)))
          (coq-compile-file-command
           (message "Compiling %s..." buffer-file-name)
-          (shell-command 
+          (shell-command
            ;; Could be run in the background here if we
            ;; added & to the end of the command.
            (format coq-compile-file-command buffer-file-name)))))))
@@ -1160,7 +1160,7 @@ This is a value for the `proof-deactivate-scripting-hook'."
 
 ;; Dependency management 1: when a buffer is retracted, we also
 ;; need to retract any children buffers.
-;; To do that, we run coqdep on each of the processed files, 
+;; To do that, we run coqdep on each of the processed files,
 ;; and see whether the buffer being retracted is an ancestor.
 
 (defun coq-ancestors-of (filename)
@@ -1170,16 +1170,16 @@ Currently this doesn't take the loadpath into account."
   ;; FIXME: is there any way to bring in the load path here in coqdep?
   ;; We might use Coq's "Locate File string." command to help.
   (let* ((filedir   (file-name-directory filename))
-         (cdline    (shell-command-to-string 
+         (cdline    (shell-command-to-string
                      (format "coqdep -I %s %s" filedir filename)))
          (matchdeps (string-match ": \\(.*\\)$" cdline))
          (deps      (and matchdeps
                          (split-string (match-string 1 cdline)))))
-    (mapcar 
+    (mapcar
      ;; normalise to include directories, defaulting
      ;; to same dir.  Change .vo -> v
      (lambda (file)
-       (concat 
+       (concat
         (if (file-name-directory file) "" filedir)
         (file-name-sans-extension file) ".v"))
      ;; first dep is vacuous: file itself
@@ -1198,8 +1198,8 @@ Currently this doesn't take the loadpath into account."
     all))
 
 ;; FIXME: add other cases, move to coq-syntax
-(defconst coq-require-command-regexp 
-  (concat "Require\\s-+\\(" proof-id "\\)")  
+(defconst coq-require-command-regexp
+  (concat "Require\\s-+\\(" proof-id "\\)")
   "Regular expression matching Require commands in Coq.
 Group number 1 matches the name of the library which is required.")
 
@@ -1248,7 +1248,7 @@ Group number 1 matches the name of the library which is required.")
   (cond
    (coq-time-commands
     (setq string (concat "Time " string)))))
-      
+
 (add-hook 'proof-shell-insert-hook 'coq-preprocessing)
 
 
@@ -1264,7 +1264,7 @@ Group number 1 matches the name of the library which is required.")
 This is a horrible and approximate way of doing subterm markup.
 \(Code used to be in Coq, but got lost between versions 5 and 7).
 This is a hook setting for `pg-after-fontify-output-hook' to
-enable identifiers to be highlighted and allow useful 
+enable identifiers to be highlighted and allow useful
 mouse activation."
   (goto-char (point-min))
   (while (re-search-forward "\(\w+[^\w]\)" nil t)
@@ -1272,7 +1272,7 @@ mouse activation."
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;
-;; Context-senstive in-span menu additions 
+;; Context-senstive in-span menu additions
 ;;
 
 ;; da: message to Pierre: I just put these in as examples,
@@ -1285,11 +1285,11 @@ mouse activation."
       (let ((thm (span-property span 'name)))
         (list (vector
                "Check"
-               `(proof-shell-invisible-command 
+               `(proof-shell-invisible-command
                  ,(format "Check %s." thm)))
               (vector
                "Print Proof"
-               `(proof-shell-invisible-command 
+               `(proof-shell-invisible-command
                  ,(format "Print Proof %s." thm)))))))
 
 
@@ -1297,7 +1297,7 @@ mouse activation."
 ; Some smart insertion function
 ;;;;;;;;;;;;;;;;;;;;;;
 
-(defconst module-kinds-table 
+(defconst module-kinds-table
   '(("Section" 0) ("Module" 1) ("Module Type" 2) ("Declare Module" 3))
   "Enumerates the different kinds of modules.")
 
@@ -1308,12 +1308,12 @@ mouse activation."
 (defun coq-insert-section-or-module ()
   "Insert a module or a section after asking right questions."
   (interactive)
-  (let* 
+  (let*
       ((mods (completing-read "kind of module (tab to see list): " module-kinds-table))
        (s (read-string  "Name: "))
        (typkind (if (string-equal mods "Section")
                     "" ;; if not a section
-                  (completing-read "kind of type (optional, tab to see list): " 
+                  (completing-read "kind of type (optional, tab to see list): "
                                    modtype-kinds-table)))
        (p (point)))
     (if (string-equal typkind "")
@@ -1336,9 +1336,9 @@ mouse activation."
 (defun coq-insert-requires ()
   "Insert requires to modules, iteratively."
   (interactive)
-  (let* ((s) 
-         (reqkind 
-          (completing-read "Command (tab to see list, default Require Export) : " 
+  (let* ((s)
+         (reqkind
+          (completing-read "Command (tab to see list, default Require Export) : "
                            reqkinds-kinds-table nil nil nil nil "Require Export"))
          )
     (setq s (read-string  "Name (empty to stop) : "))
@@ -1353,17 +1353,17 @@ mouse activation."
   "Ends a Coq section."
   (interactive)
   (let ((count 1)) ; The number of section already "Ended" + 1
-    (let ((section 
-	   (save-excursion 
-	     (progn 
-	       (while (and (> count 0) 
-			   (search-backward-regexp 
+    (let ((section
+	   (save-excursion
+	     (progn
+	       (while (and (> count 0)
+			   (search-backward-regexp
 			    "Chapter\\|Section\\|End" 0 t))
 		 (if (char-equal (char-after (point)) ?E)
 		     (setq count (1+ count))
 		   (setq count (1- count))))
 	       (buffer-substring-no-properties
-          (progn (beginning-of-line) (forward-word 1) (point)) 
+          (progn (beginning-of-line) (forward-word 1) (point))
           (progn (end-of-line) (point)))))))
       (insert (concat "End" section)))))
 
@@ -1372,9 +1372,9 @@ mouse activation."
 Based on idea mentioned in Coq reference manual."
   (interactive)
   (let* ((shints (proof-shell-invisible-cmd-get-result "Show Intros."))
-         (intros (replace-in-string shints "^\\([^\n]+\\)\n" "intros \\1.")))
+         (intros (replace-regexp-in-string "^\\([^\n]+\\)\n"  "intros \\1." shints)))
     (if (or (< (length shints) 2);; empty response is just NL
-            (string-match coq-error-regexp shints)) 
+            (string-match coq-error-regexp shints))
         (error "Don't know what to intro. ")
       (insert intros)
       (indent-according-to-mode))))
@@ -1392,8 +1392,8 @@ tactical.  Based on idea mentioned in Coq reference manual."
   (proof-assert-next-command-interactive)
   (remove-hook 'proof-shell-insert-hook 'coq-insert-infoH-hook);as soone as possible
   (proof-shell-wait)
-  (let 
-      ((str (string-match "<info type=\"infoH\">\\([^<]*\\)</info>" 
+  (let
+      ((str (string-match "<info type=\"infoH\">\\([^<]*\\)</info>"
                           coq-last-hybrid-pre-string))
        (substr (match-string 1 coq-last-hybrid-pre-string))
        )
@@ -1410,13 +1410,13 @@ tactical.  Based on idea mentioned in Coq reference manual."
 Based on idea mentioned in Coq reference manual. Also insert holes at insertion
 positions."
   (interactive)
-  (proof-shell-ready-prover) 
+  (proof-shell-ready-prover)
   (let* ((cmd))
     (setq cmd (read-string "Build match for type:"))
-    (let* ((thematch 
+    (let* ((thematch
            (proof-shell-invisible-cmd-get-result (concat "Show Match " cmd ".")))
-          (match (replace-in-string thematch "=> \n" "=> #\n")))
-      ;; if error, it will be displayed in response buffer (see def of 
+           (match (replace-regexp-in-string "=> \n" "=> #\n" thematch)))
+      ;; if error, it will be displayed in response buffer (see def of
       ;; proof-shell-invisible-cmd-get-result), otherwise:
       (unless (proof-string-match coq-error-regexp match)
         (let ((start (point)))
@@ -1430,7 +1430,7 @@ positions."
 	 (holes-set-point-next-hole-destroy)) ; if only one hole, go to it.
 	(t
 	 (goto-char start)
-	 (message 
+	 (message
           (substitute-command-keys
            "\\[holes-set-point-next-hole-destroy] to jump to active hole.  \\[holes-short-doc] to see holes doc.")))))
           )))))
@@ -1630,15 +1630,15 @@ number of hypothesis displayed, without hiding the goal"
 (defvar coq-modeline-string1 " SUBGOAL* ")
 (defvar coq-modeline-string0 " Scripting *")
 (defun coq-build-subgoals-string (n)
-  (concat coq-modeline-string0 (int-to-string n) 
-          (if (> n 1) coq-modeline-string2 
+  (concat coq-modeline-string0 (int-to-string n)
+          (if (> n 1) coq-modeline-string2
             coq-modeline-string1)))
 
 (defun coq-update-minor-mode-alist ()
   "Modify `minor-mode-alist' to display the number of subgoals in the modeline."
   (save-window-excursion ; switch to buffer even if not visible
     (switch-to-buffer proof-goals-buffer)
-    (let* ((nbgoals (string-to-int (first-word-of-buffer)))
+    (let* ((nbgoals (string-to-number (first-word-of-buffer)))
            (toclean (assq 'proof-active-buffer-fake-minor-mode minor-mode-alist)))
       (while toclean ;; clean minor-mode-alist
         (setq minor-mode-alist (remove toclean minor-mode-alist))
@@ -1672,10 +1672,10 @@ number of hypothesis displayed, without hiding the goal"
 (defun optim-resp-windows ()
   "Resize response buffer to optimal size.
 Only when three-buffer-mode is enabled."
-  (when (and proof-three-window-enable 
+  (when (and proof-three-window-enable
              (> (frame-height) 10)
              (get-buffer-window proof-response-buffer))
-    (let ((curwin (selected-window)) 
+    (let ((curwin (selected-window))
           ;; maxhgth is the max height of both resp and goals buffers to avoid
           ;; make the other disappear
           (maxhgth (- (window-height) window-min-height))