Merge branch 'master' of github.com:ProofGeneral/PG

27 files changed, 694 insertions, 742 deletions

diff --git a/acl2/acl2.el b/acl2/acl2.el
index cf9f521c..db3120ed 100644
--- a/acl2/acl2.el
+++ b/acl2/acl2.el
@@ -3,7 +3,7 @@
 ;; This file is part of Proof General.
 
 ;; Portions © Copyright 1994-2012  David Aspinall and University of Edinburgh
-;; Portions © Copyright 2003, 2012, 2014  Free Software Foundation, Inc.
+;; Portions © Copyright 2003-2018  Free Software Foundation, Inc.
 ;; Portions © Copyright 2001-2017  Pierre Courtieu
 ;; Portions © Copyright 2010, 2016  Erik Martin-Dorel
 ;; Portions © Copyright 2011-2013, 2016-2017  Hendrik Tews
@@ -24,10 +24,9 @@
 (require 'proof-easy-config)            ; easy configure mechanism
 (require 'proof-syntax)			; functions for making regexps
 
-(setq auto-mode-alist                   ; ACL2 uses two file extensions
-      (cons				; Only grab .lisp extension after
-       (cons "\\.lisp$" 'acl2-mode)	; an acl2 file has been loaded
-       auto-mode-alist))
+(add-to-list 'auto-mode-alist                ; ACL2 uses two file extensions
+                                             ; Only grab .lisp extension after
+             (cons "\\.lisp\\'" 'acl2-mode)) ; an acl2 file has been loaded
 
 (proof-easy-config  'acl2 "ACL2"
  proof-assistant-home-page       "http://www.cs.utexas.edu/users/moore/acl2"
diff --git a/coq/coq-abbrev.el b/coq/coq-abbrev.el
index 308ca865..a15db325 100644
--- a/coq/coq-abbrev.el
+++ b/coq/coq-abbrev.el
@@ -1,9 +1,9 @@
-;;; coq-abbrev.el --- coq abbrev table and menus for ProofGeneral mode
+;;; coq-abbrev.el --- coq abbrev table and menus for ProofGeneral mode  -*- lexical-binding:t -*-
 
 ;; This file is part of Proof General.
 
 ;; Portions © Copyright 1994-2012  David Aspinall and University of Edinburgh
-;; Portions © Copyright 2003, 2012, 2014  Free Software Foundation, Inc.
+;; Portions © Copyright 2003-2018  Free Software Foundation, Inc.
 ;; Portions © Copyright 2001-2017  Pierre Courtieu
 ;; Portions © Copyright 2010, 2016  Erik Martin-Dorel
 ;; Portions © Copyright 2011-2013, 2016-2017  Hendrik Tews
@@ -68,46 +68,10 @@
 
 ;;; The abbrev table built from keywords tables
 ;#s and @{..} are replaced by holes by holes-abbrev-complete
-(defun coq-install-abbrevs ()
-  "Install default abbrev table for coq if no other already is."
-  (if (boundp 'coq-mode-abbrev-table)
-      ;; da: this test will always fail.  Assume bound-->non-empty
-      ;; (not (equal coq-mode-abbrev-table (make-abbrev-table))))
-      (message "Coq abbrevs already exists, default not loaded")
-    (define-abbrev-table 'coq-mode-abbrev-table
-      (append coq-tactics-abbrev-table coq-tacticals-abbrev-table
-              coq-commands-abbrev-table coq-terms-abbrev-table))
-    ;; if we use default coq abbrev, never ask to save it
-    ;; PC: fix trac #382 I comment this. But how to disable abbrev
-    ;; saving for coq mode only?
-    ;;(setq save-abbrevs nil) ; 
-    ;; DA: how about above, just temporarily disable saving?
-    (message "Coq default abbrevs loaded")))
-
-(unless (or noninteractive (bound-and-true-p byte-compile-current-file))
-  (coq-install-abbrevs))
-;;;;;
-
-; Redefining this macro to change the way a string option is asked to
-; the user: we pre fill the answer with current value of the option;
-(defun proof-defstringset-fn (var &optional othername)
-  "Define a function <VAR>-toggle for setting an integer customize setting VAR.
-Args as for the macro `proof-defstringset', except will be evaluated."
-  (eval
-   `(defun ,(if othername othername
-	      (intern (concat (symbol-name var) "-stringset"))) (arg)
-	      ,(concat "Set `" (symbol-name var) "' to ARG.
-This function simply uses customize-set-variable to set the variable.
-It was constructed with `proof-defstringset-fn'.")
-;	      (interactive ,(format "sValue for %s (a string, currenly %s): "
-;				    (symbol-name var) (symbol-value var)))
-	      (interactive (list
-			    (read-string
-			     (format "Value for %s (float): "
-				     (symbol-name (quote ,var))
-				     (symbol-value (quote ,var)))
-			     (symbol-value (quote ,var)))))
-	      (customize-set-variable (quote ,var) arg))))
+(define-abbrev-table 'coq-mode-abbrev-table
+  (append coq-tactics-abbrev-table coq-tacticals-abbrev-table
+          coq-commands-abbrev-table coq-terms-abbrev-table)
+  "Abbrev table for Coq.")
 
 ;; The coq menu partly built from tables
 
diff --git a/coq/coq-autotest.el b/coq/coq-autotest.el
index 8be4bed9..5ca66706 100644
--- a/coq/coq-autotest.el
+++ b/coq/coq-autotest.el
@@ -1,4 +1,4 @@
-;;; coq-autotest.el --- tests of Coq Proof General (in progress).
+;;; coq-autotest.el --- tests of Coq Proof General (in progress)  -*- lexical-binding:t -*-
 
 ;; This file is part of Proof General.
 
@@ -21,7 +21,9 @@
 (require 'proof-site)
 (defvar coq-compile-before-require)
 
-(unless (bound-and-true-p byte-compile-current-file)
+;;;###autoload
+(defun coq-autotest ()
+  (interactive)
 
   (pg-autotest start 'debug)
 
diff --git a/coq/coq-db.el b/coq/coq-db.el
index 36812c4c..7e59bffb 100644
--- a/coq/coq-db.el
+++ b/coq/coq-db.el
@@ -25,7 +25,7 @@
 
 (eval-when-compile (require 'cl-lib))   ;decf
 
-(require 'proof-config)			; for proof-face-specs, a macro
+(require 'proof-config)
 (require 'proof-syntax)			; for proof-ids-to-regexp
 (require 'holes)
 
@@ -187,7 +187,7 @@ Used by `coq-build-menu-from-db', which you should probably use instead.  See
   (let ((l db) (res ()) (size lgth)
 	(keybind-abbrev (substitute-command-keys " \\[expand-abbrev]")))
     (while (and l (> size 0))
-      (let* ((hd (car l))
+      (let* ((hd (pop l))
 	     (menu     	 (nth 0 hd)) ; e1 = menu entry
 	     (abbrev   	 (nth 1 hd)) ; e2 = abbreviation
 	     (complt   	 (nth 2 hd)) ; e3 = completion
@@ -209,10 +209,9 @@ Used by `coq-build-menu-from-db', which you should probably use instead.  See
 		  ;;insertion function if present otherwise insert completion
 		  (if insertfn insertfn `(holes-insert-and-expand ,complt))
 		  t)))
-	    (setq res (nconc res (list menu-entry)))));; append *in place*
-	(setq l (cdr l))
+	    (push menu-entry res)))
 	(cl-decf size)))
-    res))
+    (nreverse res)))
 
 
 (defun coq-build-title-menu (db size)
@@ -289,10 +288,9 @@ 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
-  (proof-face-specs
-   (:foreground "red") ; pour les fonds clairs
-   (:foreground "red1") ; pour les fonds foncés
-   ()) ; pour le noir et blanc
+  `((((background light)) :foreground "red")
+    (((background dark)) :foreground "red1")
+    ()) ; pour le noir et blanc
   "Face for names of closing tactics in proof scripts."
   :group 'proof-faces)
 
diff --git a/coq/coq-indent.el b/coq/coq-indent.el
index af780251..ba4db8c3 100644
--- a/coq/coq-indent.el
+++ b/coq/coq-indent.el
@@ -523,7 +523,7 @@ the (point-min) if there is no previous command."
   "Move to the start of command at point.
 The point is put exactly before first non comment letter of the command."
   (coq-find-current-start)
-  (coq-find-not-in-comment-forward "\\S-"))
+  (forward-comment (point-max)))
 
 (defun same-line (pt pt2)
  (or (= (line-number-at-pos pt) (line-number-at-pos pt2))))
diff --git a/coq/coq-par-compile.el b/coq/coq-par-compile.el
index c6822dc5..ac2e82bf 100644
--- a/coq/coq-par-compile.el
+++ b/coq/coq-par-compile.el
@@ -35,7 +35,7 @@
 ;;; Code:
 
 (defvar queueitems)       ; dynamic scope in p-s-extend-queue-hook
-
+(eval-when-compile (require 'cl-lib))
 (require 'coq-compile-common)
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
@@ -712,7 +712,7 @@ function returns () if MODULE-ID comes from the standard library."
           ;;            error-message)))
           ;; (coq-seq-display-compile-response-buffer)
           (error error-message)))
-    (assert (<= (length result) 1)
+    (cl-assert (<= (length result) 1)
 	    nil "Internal error in coq-seq-map-module-id-to-obj-file")
     (car-safe result)))
 
@@ -949,7 +949,7 @@ errors are reported with an error message."
 
 (defun coq-par-run-vio2vo-queue ()
   "Start delayed vio2vo compilation."
-  (assert (not coq--last-compilation-job)
+  (cl-assert (not coq--last-compilation-job)
 	  nil "normal compilation and vio2vo in parallel 3")
   (setq coq--compile-vio2vo-in-progress t)
   (setq coq--compile-vio2vo-delay-timer nil)
@@ -1011,7 +1011,7 @@ somewhere after the last require command."
 
 (defun coq-par-add-queue-dependency (dependee dependant)
   "Add queue dependency from child job DEPENDEE to parent job DEPENDANT."
-  (assert (and (not (get dependant 'queue-dependant-waiting))
+  (cl-assert (and (not (get dependant 'queue-dependant-waiting))
 	       (not (get dependee 'queue-dependant)))
 	  nil "queue dependency cannot be added")
   (put dependant 'queue-dependant-waiting t)
@@ -1202,13 +1202,13 @@ when they transition from 'waiting-queue to 'ready:
 
 This function can safely be called for non-top-level jobs. This
 function must not be called for failed jobs."
-  (assert (not (get job 'failed))
+  (cl-assert (not (get job 'failed))
 	  nil "coq-par-retire-top-level-job precondition failed")
   (let ((span (get job 'require-span))
 	(items (get job 'queueitems)))
     (when (and span coq-lock-ancestors)
       (dolist (anc-job (get job 'ancestors))
-	(assert (not (eq (get anc-job 'lock-state) 'unlocked))
+	(cl-assert (not (eq (get anc-job 'lock-state) 'unlocked))
 		nil "bad ancestor lock state")
 	(when (eq (get anc-job 'lock-state) 'locked)
 	  (put anc-job 'lock-state 'asserted)
@@ -1290,7 +1290,7 @@ case, the following actions are taken:
       (let ((dependant (get job 'queue-dependant)))
 	(if dependant
 	    (progn
-	      (assert (not (eq coq--last-compilation-job job))
+	      (cl-assert (not (eq coq--last-compilation-job job))
 		      nil "coq--last-compilation-job invariant error")
 	      (put dependant 'queue-dependant-waiting nil)
 	      (when coq--debug-auto-compilation
@@ -1309,7 +1309,7 @@ case, the following actions are taken:
 		(proof-script-clear-queue-spans-on-error nil))
 	      (proof-release-lock)
 	      (when (eq coq-compile-quick 'quick-and-vio2vo)
-		(assert (not coq--compile-vio2vo-delay-timer)
+		(cl-assert (not coq--compile-vio2vo-delay-timer)
 			nil "vio2vo timer set before last compilation job")
 		(setq coq--compile-vio2vo-delay-timer
 		      (run-at-time coq-compile-vio2vo-delay nil
@@ -1362,7 +1362,7 @@ if it reaches 0, the next transition is triggered for DEPENDANT.
 For 'file jobs this is 'waiting-dep -> 'enqueued-coqc and for
 'clone jobs this 'waiting-dep -> 'waiting-queue."
   ;(message "%s: CPDCD with time %s" (get dependant 'name) dependee-time)
-  (assert (eq (get dependant 'state) 'waiting-dep)
+  (cl-assert (eq (get dependant 'state) 'waiting-dep)
 	  nil "wrong state of parent dependant job")
   (when (coq-par-time-less (get dependant 'youngest-coqc-dependency)
 			   dependee-time)
@@ -1371,7 +1371,7 @@ For 'file jobs this is 'waiting-dep -> 'enqueued-coqc and for
        (append dependee-ancestors (get dependant 'ancestors)))
   (put dependant 'coqc-dependency-count
        (1- (get dependant 'coqc-dependency-count)))
-  (assert (<= 0 (get dependant 'coqc-dependency-count))
+  (cl-assert (<= 0 (get dependant 'coqc-dependency-count))
 	  nil "dependency count below zero")
   (when coq--debug-auto-compilation
     (message "%s: coqc dependency count down to %d"
@@ -1439,7 +1439,7 @@ This function makes the following actions.
 		       "maybe kickoff queue")
 	       (get job 'name)
 	       (if dependant-alive "some" "no")))
-    (assert (or (not (get job 'failed)) (not dependant-alive))
+    (cl-assert (or (not (get job 'failed)) (not dependant-alive))
 	    nil "failed job with non-failing dependant")
     (when (or (and (not dependant-alive)
 		   (not (get job 'require-span))
@@ -1512,7 +1512,7 @@ coqdep or coqc are started for it."
 	 (get job 'required-obj-file))))
      ((eq job-state 'ready)
       (coq-par-start-vio2vo job))
-     (t (assert nil nil "coq-par-start-task with invalid job")))))
+     (t (cl-assert nil nil "coq-par-start-task with invalid job")))))
 
 (defun coq-par-start-jobs-until-full ()
   "Start background jobs until the limit is reached."
@@ -1622,7 +1622,7 @@ Return t if job has a direct or indirect dependant that has not
 failed yet and that is in a state before 'waiting-queue. Also,
 return t if JOB has a dependant that is a top-level job which has
 not yet failed."
-  (assert (not (eq (get job 'lock-state) 'asserted))
+  (cl-assert (not (eq (get job 'lock-state) 'asserted))
 	  nil "coq-par-ongoing-compilation precondition failed")
   (cond
    ((get job 'failed)
@@ -1653,7 +1653,7 @@ not yet failed."
 	(setq res (coq-par-ongoing-compilation dep)))
       res))
    (t
-    (assert nil nil
+    (cl-assert nil nil
 	    "impossible ancestor state %s on job %s"
 	    (get job 'state) (get job 'name)))))
 
@@ -1680,7 +1680,7 @@ Mark JOB with 'queue-failed, and, if JOB is in state
 appropriate."
   (unless (or (get job 'failed) (get job 'queue-failed))
     (put job 'queue-failed t)
-    (assert (not (eq (get job 'state) 'ready))
+    (cl-assert (not (eq (get job 'state) 'ready))
 	    nil "coq-par-mark-queue-failing impossible state")
     (when coq--debug-auto-compilation
       (message "%s: mark as queue-failed, %s"
@@ -1893,7 +1893,7 @@ there is no last compilation job."
     ;; add the asserted items to the last compilation job
     (if coq--last-compilation-job
 	(progn
-	  (assert (not (coq-par-job-is-ready coq--last-compilation-job))
+	  (cl-assert (not (coq-par-job-is-ready coq--last-compilation-job))
 		  nil "last compilation job from previous compilation ready")
 	  (put coq--last-compilation-job 'queueitems
 	       (nconc (get coq--last-compilation-job 'queueitems)
@@ -1979,7 +1979,7 @@ the maximal number of background compilation jobs is started."
 	(cancel-timer coq--compile-vio2vo-delay-timer)
 	(setq coq--compile-vio2vo-delay-timer nil))
       (when coq--compile-vio2vo-in-progress
-	(assert (not coq--last-compilation-job)
+	(cl-assert (not coq--last-compilation-job)
 		nil "normal compilation and vio2vo in parallel 2")
 	;; there are only vio2vo background processes
 	(coq-par-kill-all-processes)
diff --git a/coq/coq-par-test.el b/coq/coq-par-test.el
index ebc5ecd7..f2e3f01d 100644
--- a/coq/coq-par-test.el
+++ b/coq/coq-par-test.el
@@ -3,7 +3,7 @@
 ;; This file is part of Proof General.
 
 ;; Portions © Copyright 1994-2012  David Aspinall and University of Edinburgh
-;; Portions © Copyright 2003, 2012, 2014  Free Software Foundation, Inc.
+;; Portions © Copyright 2003-2018  Free Software Foundation, Inc.
 ;; Portions © Copyright 2001-2017  Pierre Courtieu
 ;; Portions © Copyright 2010, 2016  Erik Martin-Dorel
 ;; Portions © Copyright 2011-2013, 2016-2017  Hendrik Tews
@@ -31,6 +31,7 @@
 ;;; Code:
 
 (require 'coq-par-compile)
+(eval-when-compile (require 'cl-lib))
 
 (defconst coq--par-job-needs-compilation-tests
   ;; for documentation see the doc string following the init value
@@ -753,7 +754,7 @@ relative ages.")
    (lambda (test)
      (let ((test-id (format "%s" (car test))))
        ;; a test is a list of 4 elements and the first element is a list itself
-       (assert
+       (cl-assert
 	(and
 	 (eq (length test) 4)
 	 (listp (car test)))
@@ -761,22 +762,22 @@ relative ages.")
        (mapc
 	(lambda (variant)
 	  ;; a variant is a list of 4 elements
-	  (assert (eq (length variant) 4) nil (concat test-id " 2"))
+	  (cl-assert (eq (length variant) 4) nil (concat test-id " 2"))
 	  (let ((files (coq-par-test-flatten-files (car test)))
 		(quick-mode (car variant))
 		(compilation-result (nth 1 variant))
 		(delete-result (nth 2 variant))
 		(req-obj-result (nth 3 variant)))
 	    ;; the delete field, when set, must be a member of the files list
-	    (assert (or (not delete-result)
+	    (cl-assert (or (not delete-result)
 			(member delete-result files))
 		    nil (concat test-id " 3"))
 	    ;; 8.4 compatibility check
 	    (when (and (or (eq quick-mode 'no-quick) (eq quick-mode 'ensure-vo))
 		       (not (member 'vio files)))
-	      (assert (not delete-result)
+	      (cl-assert (not delete-result)
 		      nil (concat test-id " 4"))
-	      (assert (eq compilation-result
+	      (cl-assert (eq compilation-result
 			  (not (eq (car (last (car test))) 'vo)))
 		      nil (concat test-id " 5")))))
 	  (cdr test))))
@@ -789,7 +790,7 @@ relative ages.")
 	       ((eq sym 'dep) "dep.vo")
 	       ((eq sym 'vo) "a.vo")
 	       ((eq sym 'vio) "a.vio")
-	       (t (assert nil)))))
+	       (t (cl-assert nil)))))
     (concat dir "/" file)))
 
 (defun test-coq-par-one-test (counter dir file-descr variant dep-just-compiled)
@@ -832,7 +833,7 @@ test the result and side effects wth `assert'."
       ;; 	       different-counter (current-time))
       (setq different-not-ok nil)
       (setq different-counter (1- different-counter))
-      (assert (> different-counter 0)
+      (cl-assert (> different-counter 0)
 	      nil "create files with different time stamps failed")
       (dolist (same-descr file-descr)
 	(when (symbolp same-descr)
@@ -845,7 +846,7 @@ test the result and side effects wth `assert'."
 	(setq same-not-ok t)
 	(while same-not-ok
 	  (setq same-counter (1- same-counter))
-	  (assert (> same-counter 0)
+	  (cl-assert (> same-counter 0)
 		  nil "create files with same time stamp filed")
 	  (dolist (file file-list)
 	    (with-temp-file file t))
@@ -875,40 +876,40 @@ test the result and side effects wth `assert'."
       (put job 'youngest-coqc-dependency 'just-compiled))
     (setq result (coq-par-job-needs-compilation job))
     ;; check result
-    (assert (eq result compilation-result)
+    (cl-assert (eq result compilation-result)
 	    nil (concat id " result"))
     ;; check file deletion
-    (assert (or (not delete-result)
+    (cl-assert (or (not delete-result)
 		(not (file-attributes
 		      (test-coq-par-sym-to-file dir delete-result))))
 	    nil (concat id " delete file"))
     ;; check no other file is deleted
     (dolist (f file-descr-flattened)
       (unless (eq f delete-result)
-	(assert (file-attributes (test-coq-par-sym-to-file dir f))
+	(cl-assert (file-attributes (test-coq-par-sym-to-file dir f))
 		nil (format "%s non del file %s: %s"
 			    id f
 			    (test-coq-par-sym-to-file dir f)))))
     ;; check value of 'required-obj-file property
-    (assert (equal (get job 'required-obj-file)
+    (cl-assert (equal (get job 'required-obj-file)
 		   (test-coq-par-sym-to-file dir req-obj-result))
 	    nil (concat id " required-obj-file"))
     ;; check 'obj-mod-time property
     (if obj-mod-result
-	(assert
+	(cl-assert
 	 (equal
 	  (get job 'obj-mod-time)
 	  (nth 5 (file-attributes
 		  (test-coq-par-sym-to-file dir obj-mod-result))))
 	 nil (concat id " obj-mod-time non nil"))
-      (assert (not (get job 'obj-mod-time))
+      (cl-assert (not (get job 'obj-mod-time))
 	      nil (concat id " obj-mod-time nil")))
     ;; check 'use-quick property
-    (assert (eq (not (not (and compilation-result (eq req-obj-result 'vio))))
+    (cl-assert (eq (not (not (and compilation-result (eq req-obj-result 'vio))))
 		(get job 'use-quick))
 	    nil (concat id " use-quick"))
     ;; check vio2vo-needed property
-    (assert (eq
+    (cl-assert (eq
 	     (and (eq quick-mode 'quick-and-vio2vo)
 		  (eq req-obj-result 'vio)
 		  (or (eq delete-result 'vo)
diff --git a/coq/coq-seq-compile.el b/coq/coq-seq-compile.el
index 4889ccaf..3cdcd02a 100644
--- a/coq/coq-seq-compile.el
+++ b/coq/coq-seq-compile.el
@@ -24,6 +24,7 @@
 
 ;;; Code:
 
+(eval-when-compile (require 'cl-lib))
 (defvar queueitems)       ; dynamic scope in p-s-extend-queue-hook
 
 (require 'coq-compile-common)
@@ -335,8 +336,8 @@ function returns () if MODULE-ID comes from the standard library."
           ;;            error-message)))
           ;; (coq-display-compile-response-buffer)
           (error error-message)))
-    (assert (<= (length result) 1)
-            "Internal error in coq-seq-map-module-id-to-obj-file")
+    (cl-assert (<= (length result) 1)
+               "Internal error in coq-seq-map-module-id-to-obj-file")
     (car-safe result)))
 
 (defun coq-seq-check-module (coq-object-local-hash-symbol span module-id &optional from)
diff --git a/coq/coq-smie.el b/coq/coq-smie.el
index 15697354..72639bc6 100644
--- a/coq/coq-smie.el
+++ b/coq/coq-smie.el
@@ -1,9 +1,9 @@
-;;; coq-smie.el --- SMIE lexer, grammar, and indent rules for Coq
+;;; coq-smie.el --- SMIE lexer, grammar, and indent rules for Coq  -*- lexical-binding:t -*-
 
 ;; This file is part of Proof General.
 
 ;; Portions © Copyright 1994-2012  David Aspinall and University of Edinburgh
-;; Portions © Copyright 2003, 2012, 2014  Free Software Foundation, Inc.
+;; Portions © Copyright 2003-2018  Free Software Foundation, Inc.
 ;; Portions © Copyright 2001-2017  Pierre Courtieu
 ;; Portions © Copyright 2010, 2016  Erik Martin-Dorel
 ;; Portions © Copyright 2011-2013, 2016-2017  Hendrik Tews
@@ -41,7 +41,7 @@
 ;;; Code:
 
 (require 'coq-indent)
-(require 'smie nil 'noerror)
+(require 'smie)
 
 ; debugging
 ;(defmacro measure-time (&rest body)
@@ -64,21 +64,22 @@ indentation work well."
   :group 'coq)
 
 
-(defun coq-string-suffix-p (str1 str2 &optional ignore-case)
+(defalias 'coq--string-suffix-p
+  ;; Replacement for emacs < 24.4, borrowed from sindikat at
+  ;; stackoverflow efficient if bytecompiled, builtin version is
+  ;; probably better when it exists
+  (if (fboundp 'string-suffix-p)
+      'string-suffix-p
+    (lambda (str1 str2 &optional ignore-case)
   "Return non-nil if STR1 is a prefix of STR2.
 If IGNORE-CASE is non-nil, the comparison is done without paying
 attention to case differences."
   (let ((begin2 (- (length str2) (length str1)))
 	(end2 (length str2)))
     (when (< begin2 0) (setq begin2 0)) ; to avoid negative begin2
-    (eq t (compare-strings str1 nil nil str2 begin2 end2 ignore-case))))
+    (eq t (compare-strings str1 nil nil str2 begin2 end2 ignore-case))))))
+
 
-;; Replacement for emacs < 24.4, borrowed from sindikat at
-;; stackoverflow efficient if bytecompiled, builtin version is
-;; probably better when it exists
-(unless (fboundp 'string-suffix-p)
-  (fset 'string-suffix-p 'coq-string-suffix-p)
-  (declare-function string-suffix-p "smie"))
 
 ;; As any user defined notation ending with "." will break
 ;; proofgeneral synchronization anyway, let us consider that any
@@ -145,12 +146,13 @@ intros.      or        Proof foo.
 
 the token of \".\" is simply \".\"."
   (save-excursion
-    (let ((p (point)) (beg (coq-find-real-start))) ; moves to real start of command
+    (let ((p (point)))
+      (coq-find-real-start) ; Move to real start of command.
       (cond
        ((looking-at "BeginSubproof\\>") ". proofstart")
        ((looking-at "Proof\\>")
 	(forward-char 5)
-	(coq-find-not-in-comment-forward "[^[:space:]]") ;; skip spaces and comments
+        (forward-comment (point-max))
 	(if (looking-at "\\.\\|with\\|using") ". proofstart" "."))
        ((or (looking-at "Next\\s-+Obligation\\>")
 	    (coq-smie-detect-goal-command))
@@ -211,26 +213,28 @@ the token of \".\" is simply \".\"."
 
 (defun coq-backward-token-fast-nogluing-dot-friends ()
   (forward-comment (- (point)))
-  (let ((pt (point)))
-    (let* ((tok-punc (skip-syntax-backward "."))
-           (str-punc (buffer-substring-no-properties pt (point)))
-           (tok-other (if (zerop tok-punc) (skip-syntax-backward "w_'"))))
-      ;; special case: if the symbols found end by "." or ";", then consider this last letter alone as a token
-      (when (and (not (zerop tok-punc)) (string-match "\\s.+[.;]" str-punc))
-        (skip-syntax-forward ".")
-        (forward-char -1))
-      (buffer-substring-no-properties pt (point)))))
+  (let* ((pt (point))
+         (tok-punc (skip-syntax-backward "."))
+         (str-punc (buffer-substring-no-properties pt (point))))
+    (if (zerop tok-punc) (skip-syntax-backward "w_'"))
+    ;; Special case: if the symbols found end by "." or ";",
+    ;; then consider this last letter alone as a token
+    (when (and (not (zerop tok-punc)) (string-match "\\s.+[.;]" str-punc))
+      (skip-syntax-forward ".")
+      (forward-char -1))
+    (buffer-substring-no-properties pt (point))))
 
 (defun coq-forward-token-fast-nogluing-dot-friends ()
   (forward-comment (point-max))
-  (let ((pt (point)))
-    (let* ((tok-punc (skip-syntax-forward "."))
-           (str-punc (buffer-substring-no-properties pt (point)))
-           (tok-other (if (zerop tok-punc) (skip-syntax-forward "w_'"))))
-     ;; special case: if the symbols found end by "." or ";", then consider this last letter alone as a token
-     (when (and (not (zerop tok-punc)) (string-match "\\s.+[.;]" str-punc))
-       (forward-char -1))
-     (buffer-substring-no-properties pt (point)))))
+  (let* ((pt (point))
+         (tok-punc (skip-syntax-forward "."))
+         (str-punc (buffer-substring-no-properties pt (point))))
+    (if (zerop tok-punc) (skip-syntax-forward "w_'"))
+    ;; Special case: if the symbols found end by "." or ";",
+    ;; then consider this last letter alone as a token
+    (when (and (not (zerop tok-punc)) (string-match "\\s.+[.;]" str-punc))
+      (forward-char -1))
+    (buffer-substring-no-properties pt (point))))
 
 ;; ignore-between is a description of pseudo delimiters of blocks that
 ;; should be jumped when searching. There is a bad interaction when
@@ -298,8 +302,7 @@ inside parenthesis)."
 	      ; if we find something to ignore, we directly jump to the
 	      ; corresponding openner
 	      (if parop
-		  (let ((p (point))
-			(parops ; corresponding matcher may be a list
+		  (let ((parops ; corresponding matcher may be a list
 			 (if (listp (car parop)) (car parop) (cons (car parop) nil))))
 		    ; go to corresponding closer or meet "."
 		    ;(message "newpatterns = %S" (append parops (cons "." nil)))
@@ -386,9 +389,9 @@ The point should be at the beginning of the command name."
   (equal (point)
 	 (save-excursion (coq-find-real-start))))
 
-(defun coq-is-bullet-token (tok) (string-suffix-p "bullet" tok))
-(defun coq-is-subproof-token (tok) (string-suffix-p "subproof" tok))
-(defun coq-is-dot-token (tok) (or (string-suffix-p "proofstart" tok)
+(defun coq-is-bullet-token (tok) (coq--string-suffix-p "bullet" tok))
+(defun coq-is-subproof-token (tok) (coq--string-suffix-p "subproof" tok))
+(defun coq-is-dot-token (tok) (or (coq--string-suffix-p "proofstart" tok)
 			       (string-equal "." tok)))
 (defun coq-is-cmdend-token (tok)
   (or (coq-is-bullet-token tok) (coq-is-subproof-token tok) (coq-is-dot-token tok)))
@@ -509,7 +512,7 @@ The point should be at the beginning of the command name."
      ((member corresp '("Inductive" "CoInductive" "Variant")) ":= inductive")
      ((equal corresp "let") ":= let")
      ((equal corresp "where") ":= inductive") ;; inductive or fixpoint, nevermind
-     ((or (looking-back "{" nil)) ":= record")
+     ((or (eq ?\{ (char-before))) ":= record")
      (t ":=")))) ; a parenthesis stopped the search
 
 
@@ -541,8 +544,8 @@ The point should be at the beginning of the command name."
 	  (cond
 	   ((member backtok '("." "Ltac")) "; tactic")
 	   ((equal backtok nil)
-	    (if (or (looking-back "(" nil) (looking-back "\\[")
-		    (and (looking-back "{" nil)
+	    (if (or (memq (char-before) '(?\( ?\[))
+		    (and (eq (char-before) ?\{)
 			 (equal (coq-smie-backward-token) "{ subproof"))) ;; recursive call
 		"; tactic"
 	      "; record"))))))
@@ -558,10 +561,10 @@ The point should be at the beginning of the command name."
 		 (equal (coq-smie-backward-token) "; tactic")) ;; recursive
 	    "|| tactic")
 	   ;; this is wrong half of the time but should not harm indentation
-	   ((and (equal backtok nil) (looking-back "(" nil)) "||")
+	   ((and (equal backtok nil) (eq (char-before) '?\()) "||")
 	   ((equal backtok nil)
-	    (if (or (looking-back "\\[" nil)
-		    (and (looking-back "{" nil)
+	    (if (or (eq (char-before) '?\[)
+		    (and (eq (char-before) '?\{)
 			 (equal (coq-smie-backward-token) "{ subproof"))) ;; recursive call
 		"|| tactic"
 	      "||"))))))
@@ -618,7 +621,8 @@ The point should be at the beginning of the command name."
      ;;  (forward-char -1)
      ;;  (if (looking-at "{") "{ subproof" "} subproof"))
 
-     ((and (equal tok ":") (looking-back "\\<\\(constr\\|ltac\\|uconstr\\)" nil))
+     ((and (equal tok ":") (looking-back "\\<\\(constr\\|ltac\\|uconstr\\)"
+                                         (- (point) 7)))
       ": ltacconstr")
 
      ((member tok '(":=" "::="))
@@ -848,113 +852,112 @@ Typical values are 2 or 4."
 ;;   greatly simplify this file. We should ask Stefan Monnier how to
 ;;   have two grammars with smie.
 (defconst coq-smie-grammar
-  (when (fboundp 'smie-prec2->grammar)
-    (smie-prec2->grammar
-     (smie-bnf->prec2
-      '((exp
-	 (exp ":= def" exp)
-	 (exp ":=" exp) (exp ":= inductive" exp)
-	 (exp "||" exp) (exp "|" exp) (exp "=>" exp)
-	 (exp "xxx provedby" exp) (exp "as morphism" exp)
-	 (exp "with signature" exp)
-	 ("match" matchexp "with match" exp "end");expssss
-	 ("let" assigns "in let" exp) ;("eval in" assigns "in eval" exp) disabled
-	 ("fun" exp "=> fun" exp) ("if" exp "then" exp "else" exp)
-	 ("quantif exists" exp ", quantif" exp)
-	 ("forall" exp ", quantif" exp)
-	 ;;;
-	 ("(" exp ")") ("{|" exps "|}") ("{" exps "}")
-	 (exp "; tactic" exp) (exp "in tactic" exp) (exp "as" exp)
-	 (exp "by" exp) (exp "with" exp) (exp "|-" exp)
-	 (exp ":" exp) (exp ":<" exp) (exp "," exp)
-	 (exp "->" exp) (exp "<->" exp) (exp "&" exp)
-	 (exp "/\\" exp) (exp "\\/" exp)
-	 (exp "==" exp) (exp "=" exp) (exp "<>" exp) (exp "<=" exp)
-	 (exp "<" exp) (exp ">=" exp) (exp ">" exp)
-	 (exp "=?" exp) (exp "<=?" exp) (exp "<?" exp)
-	 (exp "^" exp)
-	 (exp "+" exp) (exp "-" exp)
-	 (exp "*" exp)
-	 (exp ": ltacconstr" exp)(exp ". selector" exp))
-	;; Having "return" here rather than as a separate rule in `exp' causes
-	;; it to be indented at a different level than "with".
-	(matchexp (exp) (exp "as match" exp) (exp "in match" exp)
-		  (exp "return" exp) )
-	(exps (affectrec) (exps "; record" exps))
-	(affectrec (exp ":= record" exp))
-	(assigns  (exp ":= let" exp)) ;(assigns "; record" assigns)
-
-	(moduledef (moduledecl ":= module" exp))
-	(moduledecl (exp) (exp ":" moduleconstraint)
-		    (exp "<:" moduleconstraint))
-	(moduleconstraint
-	 (exp) (exp ":= with" exp)
-	 (moduleconstraint "with module" "module" moduleconstraint))
-
-	;; To deal with indentation inside module declaration and inside
-	;; proofs, we rely on the lexer. The lexer detects "." terminator of
-	;; goal starter and returns the ". proofstart" and ". moduelstart"
-	;; tokens.
-	(bloc ("{ subproof" commands "} subproof")
-	      (". proofstart" commands  "Proof End")
-	      (". modulestart" commands  "end module" exp)
-	      (moduledecl) (moduledef)
-	      (exp))
-
-	(commands (commands "." commands)
-		  (commands "- bullet" commands)
-		  (commands "+ bullet" commands)
-		  (commands "* bullet" commands)
-		  (commands "-- bullet" commands)
-		  (commands "++ bullet" commands)
-		  (commands "** bullet" commands)
-		  (commands "--- bullet" commands)
-		  (commands "+++ bullet" commands)
-		  (commands "*** bullet" commands)
-		  (commands "---- bullet" commands)
-		  (commands "++++ bullet" commands)
-		  (commands "**** bullet" commands)
-		  ;; "with" of mutual definition should act like "."
-		  ;; same for "where" (introduction of a notation
-		  ;; after a inductive or fixpoint)
-		  (commands "with inductive" commands)
-		  (commands "with fixpoint" commands)
-		  (commands "where" commands)
-		  (bloc)))
-
-
-      ;; Resolve the "trailing expression ambiguity" as in "else x -> b".
-      ;; each line orders tokens by increasing priority
-      ;; | C x => fun a => b | C2 x => ...
-      ;;'((assoc "=>") (assoc "|")  (assoc "|-" "=> fun")) ; (assoc ", quantif")
-      '((assoc "- bullet") (assoc "+ bullet") (assoc "* bullet")
-	(assoc "-- bullet") (assoc "++ bullet") (assoc "** bullet")
-	(assoc "--- bullet") (assoc "+++ bullet") (assoc "*** bullet")
-	(assoc "---- bullet") (assoc "++++ bullet") (assoc "**** bullet")
-	(assoc ".")
-	(assoc "with inductive" "with fixpoint" "where"))
-      '((assoc ":= def" ":= inductive")
-	(assoc "|") (assoc "=>")
-	(assoc ":=")	(assoc "xxx provedby")
-	(assoc "as morphism") (assoc "with signature") (assoc "with match")
-	(assoc "in let")
-	(assoc "in eval") (assoc "=> fun") (assoc "then") (assoc ", quantif")
-	(assoc "|| tactic") ;; FIXME: detecting "+ tactic" and "|| tactic" seems impossible
-	(assoc "; tactic") (assoc "in tactic") (assoc "as" "by") (assoc "with")
-	(assoc "|-") (assoc ":" ":<") (assoc ",")
-        (assoc "else")
-        (assoc "->") (assoc "<->")
-	(assoc "&") (assoc "/\\") (assoc "\\/")
-	(assoc "==") (assoc "=") (assoc "<" ">" "<=" ">=" "<>")
-	(assoc "=?") (assoc "<=?") (assoc "<?") (assoc "^")
-	(assoc "||") ;; FIXME: detecting "+ tactic" and "|| tactic" seems impossible
-	(assoc "+") (assoc "-") (assoc "*")
-	(assoc ": ltacconstr") (assoc ". selector"))
-      '((assoc ":" ":<")  (assoc "<"))
-      '((assoc ". modulestart" "." ". proofstart") (assoc "Module def")
-	(assoc "with module" "module") (assoc ":= module")
-	(assoc ":= with")  (assoc ":" ":<"))
-      '((assoc ":= def") (assoc "; record") (assoc ":= record")))))
+  (smie-prec2->grammar
+   (smie-bnf->prec2
+    '((exp
+       (exp ":= def" exp)
+       (exp ":=" exp) (exp ":= inductive" exp)
+       (exp "||" exp) (exp "|" exp) (exp "=>" exp)
+       (exp "xxx provedby" exp) (exp "as morphism" exp)
+       (exp "with signature" exp)
+       ("match" matchexp "with match" exp "end") ;expssss
+       ("let" assigns "in let" exp) ;("eval in" assigns "in eval" exp) disabled
+       ("fun" exp "=> fun" exp) ("if" exp "then" exp "else" exp)
+       ("quantif exists" exp ", quantif" exp)
+       ("forall" exp ", quantif" exp)
+;;;
+       ("(" exp ")") ("{|" exps "|}") ("{" exps "}")
+       (exp "; tactic" exp) (exp "in tactic" exp) (exp "as" exp)
+       (exp "by" exp) (exp "with" exp) (exp "|-" exp)
+       (exp ":" exp) (exp ":<" exp) (exp "," exp)
+       (exp "->" exp) (exp "<->" exp) (exp "&" exp)
+       (exp "/\\" exp) (exp "\\/" exp)
+       (exp "==" exp) (exp "=" exp) (exp "<>" exp) (exp "<=" exp)
+       (exp "<" exp) (exp ">=" exp) (exp ">" exp)
+       (exp "=?" exp) (exp "<=?" exp) (exp "<?" exp)
+       (exp "^" exp)
+       (exp "+" exp) (exp "-" exp)
+       (exp "*" exp)
+       (exp ": ltacconstr" exp)(exp ". selector" exp))
+      ;; Having "return" here rather than as a separate rule in `exp' causes
+      ;; it to be indented at a different level than "with".
+      (matchexp (exp) (exp "as match" exp) (exp "in match" exp)
+		(exp "return" exp) )
+      (exps (affectrec) (exps "; record" exps))
+      (affectrec (exp ":= record" exp))
+      (assigns  (exp ":= let" exp))     ;(assigns "; record" assigns)
+
+      (moduledef (moduledecl ":= module" exp))
+      (moduledecl (exp) (exp ":" moduleconstraint)
+		  (exp "<:" moduleconstraint))
+      (moduleconstraint
+       (exp) (exp ":= with" exp)
+       (moduleconstraint "with module" "module" moduleconstraint))
+
+      ;; To deal with indentation inside module declaration and inside
+      ;; proofs, we rely on the lexer. The lexer detects "." terminator of
+      ;; goal starter and returns the ". proofstart" and ". moduelstart"
+      ;; tokens.
+      (bloc ("{ subproof" commands "} subproof")
+	    (". proofstart" commands  "Proof End")
+	    (". modulestart" commands  "end module" exp)
+	    (moduledecl) (moduledef)
+	    (exp))
+
+      (commands (commands "." commands)
+		(commands "- bullet" commands)
+		(commands "+ bullet" commands)
+		(commands "* bullet" commands)
+		(commands "-- bullet" commands)
+		(commands "++ bullet" commands)
+		(commands "** bullet" commands)
+		(commands "--- bullet" commands)
+		(commands "+++ bullet" commands)
+		(commands "*** bullet" commands)
+		(commands "---- bullet" commands)
+		(commands "++++ bullet" commands)
+		(commands "**** bullet" commands)
+		;; "with" of mutual definition should act like "."
+		;; same for "where" (introduction of a notation
+		;; after a inductive or fixpoint)
+		(commands "with inductive" commands)
+		(commands "with fixpoint" commands)
+		(commands "where" commands)
+		(bloc)))
+
+
+    ;; Resolve the "trailing expression ambiguity" as in "else x -> b".
+    ;; each line orders tokens by increasing priority
+    ;; | C x => fun a => b | C2 x => ...
+    ;;'((assoc "=>") (assoc "|")  (assoc "|-" "=> fun")) ; (assoc ", quantif")
+    '((assoc "- bullet") (assoc "+ bullet") (assoc "* bullet")
+      (assoc "-- bullet") (assoc "++ bullet") (assoc "** bullet")
+      (assoc "--- bullet") (assoc "+++ bullet") (assoc "*** bullet")
+      (assoc "---- bullet") (assoc "++++ bullet") (assoc "**** bullet")
+      (assoc ".")
+      (assoc "with inductive" "with fixpoint" "where"))
+    '((assoc ":= def" ":= inductive")
+      (assoc "|") (assoc "=>")
+      (assoc ":=")	(assoc "xxx provedby")
+      (assoc "as morphism") (assoc "with signature") (assoc "with match")
+      (assoc "in let")
+      (assoc "in eval") (assoc "=> fun") (assoc "then") (assoc ", quantif")
+      (assoc "|| tactic") ;; FIXME: detecting "+ tactic" and "|| tactic" seems impossible
+      (assoc "; tactic") (assoc "in tactic") (assoc "as" "by") (assoc "with")
+      (assoc "|-") (assoc ":" ":<") (assoc ",")
+      (assoc "else")
+      (assoc "->") (assoc "<->")
+      (assoc "&") (assoc "/\\") (assoc "\\/")
+      (assoc "==") (assoc "=") (assoc "<" ">" "<=" ">=" "<>")
+      (assoc "=?") (assoc "<=?") (assoc "<?") (assoc "^")
+      (assoc "||") ;; FIXME: detecting "+ tactic" and "|| tactic" seems impossible
+      (assoc "+") (assoc "-") (assoc "*")
+      (assoc ": ltacconstr") (assoc ". selector"))
+    '((assoc ":" ":<")  (assoc "<"))
+    '((assoc ". modulestart" "." ". proofstart") (assoc "Module def")
+      (assoc "with module" "module") (assoc ":= module")
+      (assoc ":= with")  (assoc ":" ":<"))
+    '((assoc ":= def") (assoc "; record") (assoc ":= record"))))
   "Parsing table for Coq.  See `smie-grammar'.")
 ;; FIXME:
 ; Record rec:Set :=     {
@@ -1010,11 +1013,11 @@ Typical values are 2 or 4."
 (defun coq-smie-rules (kind token)
   "Indentation rules for Coq.  See `smie-rules-function'.
 KIND is the situation and TOKEN is the thing w.r.t which the rule applies."
-  (case kind
-     (:elem (case token
-	      (basic proof-indent)))
-     (:close-all t)
-     (:list-intro
+  (pcase kind
+     (`:elem (pcase token
+	       (`basic proof-indent)))
+     (`:close-all t)
+     (`:list-intro
       (or (member token '("fun" "forall" "quantif exists" "with"))
 	  ;; We include "." in list-intro for the ". { .. } \n { .. }" so the
 	  ;; second {..} is aligned with the first rather than being indented as
@@ -1026,7 +1029,7 @@ KIND is the situation and TOKEN is the thing w.r.t which the rule applies."
 ;	    (forward-char 1) ; skip de "."
 ;	    (equal (coq-smie-forward-token) "{ subproof"))
 	  ))
-     (:after
+     (`:after
       (cond
        ;; Override the default indent step added because of their presence
        ;; in smie-closer-alist.
@@ -1064,7 +1067,9 @@ KIND is the situation and TOKEN is the thing w.r.t which the rule applies."
 		 (not (coq-smie-is-ltacdef))
 		 (not (coq-smie-is-inside-parenthesized-tactic))
 		 (or (not (smie-rule-parent-p "; tactic"))
-		     (and smie--parent
+                     ;; FIXME: Don't depend on SMIE's internals!
+		     (and (boundp 'smie--parent)
+                          smie--parent
 			  (coq-smie--same-line-as-parent
 			   (nth 1 smie--parent) (point)))))
 	    coq-indent-semicolon-tactical
@@ -1089,7 +1094,7 @@ KIND is the situation and TOKEN is the thing w.r.t which the rule applies."
 	(save-excursion (forward-char -1) (coq-find-real-start)
 			`(column . ,(+ coq-indent-modulestart (current-column)))))))
 
-     (:before
+     (`:before
       (cond
 
 ;       ((and (member token '("{ subproof"))
diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el
index bb32fc52..7a11a43f 100644
--- a/coq/coq-syntax.el
+++ b/coq/coq-syntax.el
@@ -1,9 +1,9 @@
-;;; coq-syntax.el --- Font lock expressions for Coq
+;;; coq-syntax.el --- Font lock expressions for Coq  -*- lexical-binding:t -*-
 
 ;; This file is part of Proof General.
 
 ;; Portions © Copyright 1994-2012  David Aspinall and University of Edinburgh
-;; Portions © Copyright 2003, 2012, 2014  Free Software Foundation, Inc.
+;; Portions © Copyright 2003-2018  Free Software Foundation, Inc.
 ;; Portions © Copyright 2001-2017  Pierre Courtieu
 ;; Portions © Copyright 2010, 2016  Erik Martin-Dorel
 ;; Portions © Copyright 2011-2013, 2016-2017  Hendrik Tews
@@ -19,6 +19,7 @@
 
 ;;; Code:
 
+(eval-when-compile (require 'cl-lib))
 (require 'proof-syntax)
 (require 'proof-utils)                  ; proof-locate-executable
 (require 'coq-db)
@@ -509,12 +510,12 @@ so for the following reasons:
   )
 
 ;; modules and section are indented like goal starters
-;;; PC TODO: this category is used only for indentation, because
-;;; scripting uses information from coq to decide if a goal is
-;;; started. Since it is impossible for some commands to know
-;;; syntactically if they start something (ex: Instance), the
-;;; right thing to do would be to indent only on "Proof." and forget
-;;; about this category for indentation.
+;; PC TODO: this category is used only for indentation, because
+;; scripting uses information from coq to decide if a goal is
+;; started. Since it is impossible for some commands to know
+;; syntactically if they start something (ex: Instance), the
+;; right thing to do would be to indent only on "Proof." and forget
+;; about this category for indentation.
 
 (defvar coq-goal-starters-db
   '(
@@ -986,14 +987,15 @@ so for the following reasons:
 ;;      elle declare un module.
 ;;    (la fonction vernac_declare_module dans toplevel/vernacentries)
 
-(defun coq-count-match (regexp strg)
-  "Count the number of max. non-overlapping substring of STRG matching REGEXP.
+(defun coq-count-match (regexp str)
+  "Count the number of max. non-overlapping substring of STR matching REGEXP.
 Empty matches 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)))))
+  (let ((nbmatch 0) (pos 0) (end (length str))
+        (case-fold-search nil))
+    (while (and (< pos end)
+                (string-match regexp str pos))
+      (cl-incf nbmatch)
+      (setq pos (max (match-end 0) (1+ pos))))
     nbmatch))
 
 ;; Module and or section openings are detected syntactically. Module
@@ -1008,12 +1010,16 @@ 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)))
-    (and (proof-string-match "\\`\\(Module\\)\\_>" str)
+         (affect (coq-count-match ":=" str))
+         (case-fold-search nil))
+    (and (string-match "\\`\\(Module\\)\\_>" str)
          (= letwith affect))))
 
 (defun coq-section-command-p (str)
-  (proof-string-match "\\`\\(Section\\|Chapter\\)\\_>" str))
+  (let ((case-fold-search nil))
+    (string-match "\\`\\(Section\\|Chapter\\)\\_>" str)))
+
+(defvar coq-goal-command-regexp)
 
 ;; unused anymore (for good)
 (defun coq-goal-command-str-p (str)
@@ -1022,16 +1028,17 @@ Use ‘coq-goal-command-p’ on a span instead if possible."
   (let* ((match (coq-count-match "\\_<match\\_>" str))
          (with (- (coq-count-match "\\_<with\\_>" str) (coq-count-match "\\_<with\\s-+signature\\_>" str)))
          (letwith (+ (coq-count-match "\\_<let\\_>" str) (- with match)))
-         (affect (coq-count-match ":=" str)))
-    (and (proof-string-match coq-goal-command-regexp str)
+         (affect (coq-count-match ":=" str))
+         (case-fold-search nil))
+    (and (string-match coq-goal-command-regexp str)
          (not
           (and
-           (proof-string-match
+           (string-match
             (concat "\\`\\(Local\\|Definition\\|Lemma\\|Theorem\\|Fact\\|Add\\|Let\\|Program\\|Module\\|Class\\|Instance\\)\\_>")
             str)
            (not (= letwith affect))))
-         (not (proof-string-match "\\`Declare\\s-+Module\\(\\w\\|\\s-\\|<\\)*:"
-                                  str)))))
+         (not (string-match "\\`Declare\\s-+Module\\(\\w\\|\\s-\\|<\\)*:"
+                            str)))))
 
 ;; This is the function that tests if a SPAN is a goal start. All it
 ;; has to do is look at the 'goalcmd attribute of the span.
@@ -1062,8 +1069,15 @@ It is used:
   (append coq-keywords-save-strict '("Proof"))
   )
 
+;; According to Coq, "Definition" is both a declaration and a goal.
+;; 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
+   (concat "\\(?:Time\\s-+\\)?\\(" (proof-ids-to-regexp coq-keywords-save-strict)
+           "\\)")))
 
-(defun coq-save-command-p (span str)
+(defun coq-save-command-p (_span str)
   "Decide whether argument is a Save command or not."
   (or (proof-string-match coq-save-command-regexp-strict str)
       (and (proof-string-match "\\`Proof\\_>" str)
@@ -1150,8 +1164,10 @@ It is used:
 ;; FIXME: actually these are not exactly reserved keywords, find
 ;; another classification of keywords.
 (defvar coq-reserved-regexp
-  (concat "\\_<with\\s-+signature\\_>\\|"
-   (proof-ids-to-regexp coq-reserved)))
+  (concat "\\_<"
+          "\\(?:with\\s-+signature\\|"
+          (regexp-opt coq-reserved) "\\)"
+          "\\_>"))
 
 (defvar coq-state-changing-tactics
   (coq-build-regexp-list-from-db coq-tactics-db 'filter-state-changing))
@@ -1275,16 +1291,6 @@ It is used:
   "*Font-lock table for Coq terms.")
 
 
-
-;; According to Coq, "Definition" is both a declaration and a goal.
-;; 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
-   (concat "\\(?:Time\\s-+\\)?\\(" (proof-ids-to-regexp coq-keywords-save-strict)
-           "\\)")))
-
-
 (defconst coq-save-command-regexp
   (proof-anchor-regexp
    (concat "\\(?:Time\\s-+\\)?\\(" (proof-ids-to-regexp coq-keywords-save)
@@ -1401,7 +1407,8 @@ part of another hypothesis.")
                         (search-forward-regexp coq-hyp-name-or-goalsep-in-goal-or-response-regexp nil t)
                         (goto-char (match-beginning 1))
                         ;; if previous is a newline, don't include it i the overklay
-                        (when (looking-back "\\s-") (goto-char (- (point) 1)))
+                        (when (looking-back "\\s-" (1- (point)))
+                          (goto-char (- (point) 1)))
                         (point))))
             ; if several hyp names, we name the overlays with the first hyp name
             (setq res
diff --git a/coq/coq.el b/coq/coq.el
index dfe519ef..06a01855 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -28,8 +28,6 @@
   (require 'outline)
   (require 'newcomment)
   (require 'etags))
-(defvar smie-indent-basic)
-(defvar smie-rules-function)
 (defvar proof-info)       ; dynamic scope in proof-tree-urgent-action
 (defvar action)       ; dynamic scope in coq-insert-as stuff
 (defvar string)       ; dynamic scope in coq-insert-as stuff
@@ -51,17 +49,6 @@
 (require 'coq-seq-compile)              ; sequential compilation of Requires
 (require 'coq-par-compile)              ; parallel compilation of Requires
 
-;; for compilation in Emacs < 23.3 (NB: declare function only works at top level)
-(declare-function smie-bnf->prec2 "smie")
-(declare-function smie-rule-parent-p "smie")
-(declare-function smie-default-forward-token "smie")
-(declare-function smie-default-backward-token "smie")
-(declare-function smie-rule-prev-p "smie")
-(declare-function smie-rule-separator "smie")
-(declare-function smie-rule-parent "smie")
-
-(declare-function some "cl-extra")      ; spurious bytecomp warning
-
 ;; prettify is in emacs > 24.4
 ;; FIXME: this should probably be done like for smie above.
 (defvar coq-may-use-prettify (fboundp 'prettify-symbols-mode))
@@ -331,17 +318,7 @@ See also option `coq-hide-additional-subgoals'."
 
 ;; Indentation and navigation support via SMIE.
 
-(defcustom coq-use-smie t
-  "OBSOLETE.  smie code is always used now.
-
-If non-nil, Coq mode will try to use SMIE for indentation.
-SMIE is a navigation and indentation framework available in Emacs >= 23.3."
-  :type 'boolean
-  :group 'coq)
-
-(require 'smie nil 'noerror)
-(require 'coq-smie nil 'noerror)
-
+(require 'coq-smie)
 
 ;;
 ;; Auxiliary code for Coq modes
@@ -352,8 +329,8 @@ SMIE is a navigation and indentation framework available in Emacs >= 23.3."
   "Return a list of frames displaying both response and goals buffers."
   (let* ((wins-resp (get-buffer-window-list proof-response-buffer nil t))
          (wins-gls (get-buffer-window-list proof-goals-buffer nil t))
-         (frame-resp (cl-mapcar 'window-frame wins-resp))
-         (frame-gls (cl-mapcar 'window-frame wins-gls)))
+         (frame-resp (mapcar #'window-frame wins-resp))
+         (frame-gls (mapcar #'window-frame wins-gls)))
     (filtered-frame-list (lambda (x) (and (member x frame-resp) (member x frame-gls))))))
 
 
@@ -683,7 +660,7 @@ If locked span already has a state number, then do nothing. Also updates
 ;; This hook seems the one we want.
 ;; WARNING! It is applied once after each command PLUS once before a group of
 ;; commands is started
-(add-hook 'proof-state-change-hook 'coq-set-state-infos)
+(add-hook 'proof-state-change-hook #'coq-set-state-infos)
 
 
 (defun count-not-intersection (l notin)
@@ -1028,7 +1005,7 @@ UNSETCMD.  See `coq-command-with-set-unset'."
   (concat " -\"" s "\""))
 
 (defun coq-build-removed-patterns (l)
-  (mapcar 'coq-build-removed-pattern l))
+  (mapcar #'coq-build-removed-pattern l))
 
 (defsubst coq-put-into-quotes (s)
   (concat "\"" s "\""))
@@ -1219,10 +1196,10 @@ Printing All set."
   (setq symb val) ;; FIXME this is wrong (it should be 'set', but it would set nil sometimes)
   (if coq-auto-adapt-printing-width
       (progn
-        (add-hook 'proof-assert-command-hook 'coq-adapt-printing-width)
-        (add-hook 'proof-retract-command-hook 'coq-reset-printing-width))
-    (remove-hook 'proof-assert-command-hook 'coq-adapt-printing-width)
-    (remove-hook 'proof-retract-command-hook 'coq-reset-printing-width)))
+        (add-hook 'proof-assert-command-hook #'coq-adapt-printing-width)
+        (add-hook 'proof-retract-command-hook #'coq-reset-printing-width))
+    (remove-hook 'proof-assert-command-hook #'coq-adapt-printing-width)
+    (remove-hook 'proof-retract-command-hook #'coq-reset-printing-width)))
 
 ;; In case of nested proofs (which are announced as obsolete in future versions
 ;; of coq) Coq does not show the goals of enclosing proof when closing a nested
@@ -1258,13 +1235,13 @@ be called and no command will be sent to Coq."
      ;; silent (there is no goal to show).
      (string-match "Backtrack" cmd))
     (list "Unset Silent."))))
-  
+
 (defpacustom auto-adapt-printing-width t
   "If non-nil, adapt automatically printing width of goals window.
 Each timme the user sends abunch of commands to Coq, check if the
 width of the goals window changed, and adapt coq printing width.
 WARNING: If several windows are displaying the goals buffer, one
-is chosen randomly. WARNING 2: when backtracking the printing
+is chosen arbitrarily.  WARNING 2: when backtracking the printing
 width is synchronized by coq (?!)."
   :type 'boolean
   :safe 'booleanp
@@ -1278,7 +1255,7 @@ width is synchronized by coq (?!)."
 ;; this initiates auto adapt printing width at start, by reading the config
 ;; var. Let us put this at the end of hooks to have a chance to read local
 ;; variables first.
-(add-hook 'coq-mode-hook 'coq-auto-adapt-printing-width t)
+(add-hook 'coq-mode-hook #'coq-auto-adapt-printing-width t)
 
 (defvar coq-shell-current-line-width nil
   "Current line width of the Coq printing width.
@@ -1347,7 +1324,7 @@ redisplayed."
       (proof-shell-invisible-command (format "Set Printing Width %S." (- wdth 1)) t)
       (setq coq-shell-current-line-width wdth)
       ;; Show iff show non nil and some proof is under way
-      (when (and show (not (null (caddr (coq-last-prompt-info-safe)))))
+      (when (and show (not (null (cl-caddr (coq-last-prompt-info-safe)))))
         (proof-shell-invisible-command (format "Show.") t nil 'no-error-display)))))
 
 (defun coq-adapt-printing-width-and-show(&optional show width)
@@ -1453,9 +1430,9 @@ Maintained by a hook in `proof-shell-handle-delayed-output-hook'.")
          (positions (cdr hyp-positions))
          (begcross (car positions))
          (beghypname (cadr positions))
-         (endhypname (caddr positions))
-         (beg (cadddr positions))
-         (end (cadddr (cdr positions))))
+         (endhypname (cl-caddr positions))
+         (beg (cl-cadddr positions))
+         (end (cl-cadddr (cdr positions))))
     (let ((hypnameov (coq-make-hypname-overlay beghypname endhypname fstname buf))
           (hypov (coq-make-hyp-overlay beg end fstname buf))
           (crosshypov (coq-make-hypcross-overlay begcross (+ 1 begcross) fstname buf))
@@ -1568,10 +1545,10 @@ use `coq-unhighlight-hyp' to unhilight."
     (coq-unhighlight-hyp-aux h)))
 
 (defun coq-highlight-hyps (lh)
-  (mapc 'coq-highlight-hyp lh))
+  (mapc #'coq-highlight-hyp lh))
 
 (defun coq-unhighlight-hyps (lh)
-  (mapc 'coq-unhighlight-hyp-aux lh))
+  (mapc #'coq-unhighlight-hyp-aux lh))
 
 (defun coq-highlight-selected-hyps ()
   "Highlight all hyps stored in `coq-highlighted-hyps'.
@@ -1606,7 +1583,7 @@ See `coq-highlight-hyps-cited-in-response' and `SearchAbout'."
 Highlight always takes place in goals buffer."
   (let  ((inters (coq-get-hyps-cited-in-response)))
     (coq-unhighlight-selected-hyps)
-    (setq coq-highlighted-hyps (mapcar 'car inters))
+    (setq coq-highlighted-hyps (mapcar #'car inters))
     (coq-highlight-selected-hyps)))
 
 (defun coq-toggle-highlight-hyp (h)
@@ -1743,12 +1720,12 @@ See `coq-fold-hyp'."
 (defun coq-unfold-hyp-list (lh)
     "Fold the type of hypothesis in LH temporarily.
 See `coq-unfold-hyp-aux'."
-  (mapc 'coq-unfold-hyp-aux lh))
+  (mapc #'coq-unfold-hyp-aux lh))
 
 (defun coq-fold-hyp-list (lh)
     "Fold the type of hypothesis in LH temporarily.
 See `coq-fold-hyp-aux'."
-  (mapc 'coq-fold-hyp-aux lh))
+  (mapc #'coq-fold-hyp-aux lh))
 
 (defun coq-fold-hyps ()
     "Fold the type of hypothesis in LH durably.
@@ -1837,7 +1814,6 @@ See  `coq-fold-hyp'."
 ;; *default* value to nil.
 (custom-set-default 'proof-output-tooltips nil)
 
-;; This seems xemacs only code, remove?
 (defconst coq-prettify-symbols-alist
   '(("not"	. ?¬)
     ;; ("/\\"	. ?∧)
@@ -1966,7 +1942,7 @@ Near here means PT is either inside or just aside of a comment."
   (setq proof-assistant-home-page coq-www-home-page)
 
   (setq proof-prog-name coq-prog-name)
-  (setq proof-guess-command-line 'coq-guess-command-line)
+  (setq proof-guess-command-line #'coq-guess-command-line)
   (setq proof-prog-name-guess t)
 
   ;; We manage file saveing via coq-compile-auto-save and for coq
@@ -1991,26 +1967,25 @@ Near here means PT is either inside or just aside of a comment."
         '(coq-compile-quick coq-compile-keep-going
           coq-compile-auto-save coq-lock-ancestors))
 
-  (setq proof-goal-command-p 'coq-goal-command-p
-        proof-find-and-forget-fn 'coq-find-and-forget
-        pg-topterm-goalhyplit-fn 'coq-goal-hyp
-        proof-state-preserving-p 'coq-state-preserving-p)
+  (setq proof-goal-command-p #'coq-goal-command-p
+        proof-find-and-forget-fn #'coq-find-and-forget
+        pg-topterm-goalhyplit-fn #'coq-goal-hyp
+        proof-state-preserving-p #'coq-state-preserving-p)
 
   (setq proof-query-identifier-command "Check %s.")
   ;;TODO: from v8.5 this wold be better:
   ;;(setq proof-query-identifier-command "About %s.")
 
   (setq proof-save-command-regexp coq-save-command-regexp
-        proof-really-save-command-p 'coq-save-command-p ;pierre:deals with Proof <term>.
+        proof-really-save-command-p #'coq-save-command-p ;pierre:deals with Proof <term>.
 	proof-save-with-hole-regexp coq-save-with-hole-regexp
 	proof-goal-with-hole-regexp coq-goal-with-hole-regexp
 	proof-nested-undo-regexp coq-state-changing-commands-regexp
         proof-script-imenu-generic-expression coq-generic-expression)
 
-  (when (fboundp 'smie-setup) ; always use smie, old indentation code removed
-    (smie-setup coq-smie-grammar #'coq-smie-rules
-                  :forward-token #'coq-smie-forward-token
-                  :backward-token #'coq-smie-backward-token))
+  (smie-setup coq-smie-grammar #'coq-smie-rules
+              :forward-token #'coq-smie-forward-token
+              :backward-token #'coq-smie-backward-token)
 
   ;; old indentation code.
   ;; (require 'coq-indent)
@@ -2069,7 +2044,7 @@ Near here means PT is either inside or just aside of a comment."
 
   (setq proof-cannot-reopen-processed-files nil)
 
-  (add-hook 'proof-activate-scripting-hook 'proof-cd-sync nil t))
+  (add-hook 'proof-activate-scripting-hook #'proof-cd-sync nil t))
 
 (defun coq-shell-mode-config ()
   (setq
@@ -2199,13 +2174,13 @@ Near here means PT is either inside or just aside of a comment."
 
 
 ;
-;;; FIXME: to handle "printing all" properly, we should change the state
-;;; of the variables that also depend on it.
-;;; da:
+;; FIXME: to handle "printing all" properly, we should change the state
+;; of the variables that also depend on it.
+;; da:
 
-;;; pc: removed it and others of the same kind. Put an "option" menu instead,
-;;; with no state variable. To have the state we should use coq command that
-;;; output the value of the variables.
+;; pc: removed it and others of the same kind. Put an "option" menu instead,
+;; with no state variable. To have the state we should use coq command that
+;; output the value of the variables.
 ;(defpacustom print-fully-explicit nil
 ;  "Print fully explicit terms."
 ;  :type 'boolean
@@ -2335,7 +2310,7 @@ The not yet delayed output is in the region
                              proof-tree-show-subgoal))
                           proof-action-list))))))))))
   
-(add-hook 'proof-tree-urgent-action-hook 'coq-proof-tree-get-new-subgoals)
+(add-hook 'proof-tree-urgent-action-hook #'coq-proof-tree-get-new-subgoals)
 
 
 (defun coq-find-begin-of-unfinished-proof ()
@@ -2464,7 +2439,7 @@ result of `coq-proof-tree-get-proof-info'."
       ;; finished the current proof
       (coq-proof-tree-disable-evars)))))
 
-(add-hook 'proof-tree-urgent-action-hook 'coq-proof-tree-evar-display-toggle)
+(add-hook 'proof-tree-urgent-action-hook #'coq-proof-tree-evar-display-toggle)
 
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
@@ -2488,7 +2463,7 @@ result of `coq-proof-tree-get-proof-info'."
                   (coq-bullet-p string)) ;; coq does not accept "Time -".
         (setq string (concat coq--time-prefix string))))))
 
-(add-hook 'proof-shell-insert-hook 'coq-preprocessing)
+(add-hook 'proof-shell-insert-hook #'coq-preprocessing)
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;
@@ -2542,8 +2517,8 @@ mouse activation."
   (string-match-p "\\.v\\'" s))
 
 (defun coq-directories-files (l)
-  (let* ((file-list-list (mapcar 'directory-files l))
-         (file-list (apply 'append file-list-list))
+  (let* ((file-list-list (mapcar #'directory-files l))
+         (file-list (apply #'append file-list-list))
          (filtered-list (cl-remove-if-not #'coq-postfix-.v-p file-list)))
   filtered-list))
 
@@ -2558,7 +2533,7 @@ mouse activation."
          (cleanpth (mapcar #'coq-load-path-to-paths pth))
          (existingpth (cl-remove-if-not #'file-exists-p cleanpth))
          (file-list (coq-directories-files existingpth)))
-    (mapcar 'coq-remove-dot-v-extension file-list)))
+    (mapcar #'coq-remove-dot-v-extension file-list)))
 
 (defun coq-insert-section-or-module ()
   "Insert a module or a section after asking right questions."
@@ -2807,8 +2782,8 @@ Completion is on a quasi-exhaustive list of Coq tacticals."
 ;; Insertion commands
 (define-key coq-keymap [(control ?i)] 'coq-insert-intros)
 (define-key coq-keymap [(control ?m)] 'coq-insert-match)
-(define-key coq-keymap [(control ?()] 'coq-insert-section-or-module)
-(define-key coq-keymap [(control ?))] 'coq-end-Section)
+(define-key coq-keymap [(control ?\()] 'coq-insert-section-or-module)
+(define-key coq-keymap [(control ?\))] 'coq-end-Section)
 (define-key coq-keymap [(control ?t)] 'coq-insert-tactic)
 (define-key coq-keymap [?t] 'coq-insert-tactical)
 (define-key coq-keymap [?!] 'coq-insert-solve-tactic) ; will work in tty
@@ -3014,7 +2989,7 @@ buffer."
 (defun coq-highlight-error-hook ()
   (coq-highlight-error t t))
 
-(add-hook 'proof-shell-handle-error-or-interrupt-hook 'coq-highlight-error-hook t)
+(add-hook 'proof-shell-handle-error-or-interrupt-hook #'coq-highlight-error-hook t)
 
 
 ;;
@@ -3111,9 +3086,9 @@ number of hypothesis displayed, without hiding the goal"
 ;; This hook must be added before coq-optimise-resp-windows, in order to be evaluated
 ;; *after* windows resizing.
 (add-hook 'proof-shell-handle-delayed-output-hook
-	  'coq-show-first-goal)
+	  #'coq-show-first-goal)
 (add-hook 'proof-shell-handle-delayed-output-hook
-	  'coq-update-minor-mode-alist)
+	  #'coq-update-minor-mode-alist)
 (add-hook 'proof-shell-handle-delayed-output-hook
           (lambda ()
             (if (proof-string-match coq-shell-proof-completed-regexp
@@ -3133,7 +3108,7 @@ number of hypothesis displayed, without hiding the goal"
   (<= (- (frame-height) (window-height)) 2))
 
 ;; bug fixed in generic ocde, useless now:
-;(add-hook 'proof-activate-scripting-hook '(lambda () (when proof-three-window-enable (proof-layout-windows))))
+;(add-hook 'proof-activate-scripting-hook (lambda () (when proof-three-window-enable (proof-layout-windows))))
 
 ;; *Experimental* auto shrink response buffer in three windows mode. Things get
 ;; a bit messed up if the response buffer is not at the right place (below
@@ -3183,9 +3158,11 @@ Only when three-buffer-mode is enabled."
 ;; i.e. added in hook AFTER it.
 
 ;; Adapt when displaying a normal message
-(add-hook 'proof-shell-handle-delayed-output-hook 'coq-optimise-resp-windows-if-option)
+(add-hook 'proof-shell-handle-delayed-output-hook
+          #'coq-optimise-resp-windows-if-option)
 ;; Adapt when displaying an error or interrupt
-(add-hook 'proof-shell-handle-error-or-interrupt-hook 'coq-optimise-resp-windows-if-option)
+(add-hook 'proof-shell-handle-error-or-interrupt-hook
+          #'coq-optimise-resp-windows-if-option)
 
 ;;; DOUBLE HIT ELECTRIC TERMINATOR
 ;; Trying to have double hit on colon behave like electric terminator. The "."
@@ -3315,7 +3292,7 @@ priority to the former."
 ;; when "compile when require" is off. When switching scripting buffer, let us
 ;; restart the coq shell process, so that it applies local coqtop options. 
 (add-hook 'proof-deactivate-scripting-hook
-          'coq-switch-buffer-kill-proof-shell ;; this function is in coq-compile-common
+          #'coq-switch-buffer-kill-proof-shell ;; this function is in coq-compile-common
           t)
 
 
diff --git a/etc/testsuite/pg-test.el b/etc/testsuite/pg-test.el
index 2e3c2c10..2c064827 100644
--- a/etc/testsuite/pg-test.el
+++ b/etc/testsuite/pg-test.el
@@ -3,7 +3,7 @@
 ;; This file is part of Proof General.
 
 ;; Portions © Copyright 1994-2012  David Aspinall and University of Edinburgh
-;; Portions © Copyright 2003, 2012, 2014  Free Software Foundation, Inc.
+;; Portions © Copyright 2003-2018  Free Software Foundation, Inc.
 ;; Portions © Copyright 2001-2017  Pierre Courtieu
 ;; Portions © Copyright 2010, 2016  Erik Martin-Dorel
 ;; Portions © Copyright 2011-2013, 2016-2017  Hendrik Tews
@@ -14,6 +14,8 @@
 
 ;;; Code:
 
+(eval-when-compile (require 'cl-lib))
+
 (defconst pg-test-buffer "** PG test output **")
 
 (defvar pg-test-total-success-count  0)
@@ -68,8 +70,8 @@
 		  (format " %s failed: exprected result %s, got %s\n"
 			  name goodresult result))))
       (if errorresult
-	  (incf pg-test-suite-fail-count)
-	(incf pg-test-suite-success-count)
+	  (cl-incf pg-test-suite-fail-count)
+	(cl-incf pg-test-suite-success-count)
 	(setq errorresult (format " %s succeeded.\n" name)))
       ;; Return string
       errorresult))
diff --git a/generic/pg-autotest.el b/generic/pg-autotest.el
index e7cb19a9..7a22c9f7 100644
--- a/generic/pg-autotest.el
+++ b/generic/pg-autotest.el
@@ -3,7 +3,7 @@
 ;; This file is part of Proof General.
 
 ;; Portions © Copyright 1994-2012  David Aspinall and University of Edinburgh
-;; Portions © Copyright 2003, 2012, 2014  Free Software Foundation, Inc.
+;; Portions © Copyright 2003-2018  Free Software Foundation, Inc.
 ;; Portions © Copyright 2001-2017  Pierre Courtieu
 ;; Portions © Copyright 2010, 2016  Erik Martin-Dorel
 ;; Portions © Copyright 2011-2013, 2016-2017  Hendrik Tews
@@ -25,6 +25,7 @@
 
 ;;; Code:
 
+(eval-when-compile (require 'cl-lib))
 (require 'proof-splash)
 (setq proof-splash-enable nil)		; prevent splash when testing
 
@@ -215,7 +216,7 @@ completely processing the buffer as the last step."
 	 " random jump: processing whole buffer")
 	(proof-process-buffer)
 	(proof-shell-wait)
-	(decf jumps))
+	(cl-decf jumps))
 
 	((and (eq random-thing 1)
 	      (not (proof-locked-region-empty-p)))
@@ -223,7 +224,7 @@ completely processing the buffer as the last step."
 	  " random jump: retracting whole buffer")
 	 (proof-retract-buffer)
 	 (proof-shell-wait)
-	 (decf jumps))
+	 (cl-decf jumps))
 
 	(t
 	 (pg-autotest-message
@@ -241,7 +242,7 @@ completely processing the buffer as the last step."
 		    " random jump: interrupting prover")
 		   (proof-interrupt-process)))
 	     (proof-shell-wait))
-	   (decf jumps)))))
+	   (cl-decf jumps)))))
   (unless (proof-locked-region-full-p)
     (proof-process-buffer)
     (proof-shell-wait))
diff --git a/generic/pg-movie.el b/generic/pg-movie.el
index 9be95972..755d41f5 100644
--- a/generic/pg-movie.el
+++ b/generic/pg-movie.el
@@ -3,7 +3,7 @@
 ;; This file is part of Proof General.
 
 ;; Portions © Copyright 1994-2012  David Aspinall and University of Edinburgh
-;; Portions © Copyright 2003, 2012, 2014  Free Software Foundation, Inc.
+;; Portions © Copyright 2003-2018  Free Software Foundation, Inc.
 ;; Portions © Copyright 2001-2017  Pierre Courtieu
 ;; Portions © Copyright 2010, 2016  Erik Martin-Dorel
 ;; Portions © Copyright 2011-2013, 2016-2017  Hendrik Tews
@@ -30,6 +30,7 @@
 ;;
 
 ;;; Code:
+(eval-when-compile (require 'cl-lib))
 (eval-when-compile
   (require 'span)
   (require 'unicode-tokens))
@@ -72,7 +73,7 @@
 		    (t "command")))
 	 (label    (span-property span 'rawname))
 	 (frameid  (int-to-string pg-movie-frame)))
-    (incf pg-movie-frame)
+    (cl-incf pg-movie-frame)
     (pg-xml-node frame
 		 (list (pg-xml-attr frameNumber frameid))
 		 (list
diff --git a/generic/pg-pbrpm.el b/generic/pg-pbrpm.el
index 619a5d6c..b40cfff3 100644
--- a/generic/pg-pbrpm.el
+++ b/generic/pg-pbrpm.el
@@ -34,6 +34,7 @@
 
 ;;; Code:
 (require 'span)
+(eval-when-compile (require 'cl-lib))
 (eval-when-compile
   (require 'proof-utils))
 
@@ -377,10 +378,10 @@ Returns (n . s) where
     (while (and pos l (not found))
       (setq start-goal (car l))
       (setq end-goal (cadr l))
-      (setq goal-name (caddr l))
-      (setq start-concl (cadddr l))
-      (setq hyps (car (cddddr l)))
-      (setq l (cdr (cddddr l)))
+      (setq goal-name (cl-caddr l))
+      (setq start-concl (cl-cadddr l))
+      (setq hyps (car (cl-cddddr l)))
+      (setq l (cdr (cl-cddddr l)))
       (if (and (<= start-goal pos) (<= pos end-goal))
 	  (progn
 	    (setq found t)
@@ -393,9 +394,9 @@ Returns (n . s) where
 	    (while (and hyps (not found))
 	      (setq start-hyp (car hyps))
 	      (setq start-hyp-text (cadr hyps))
-	      (setq end-hyp (caddr hyps))
-	      (setq hyp-name (cadddr hyps))
-	      (setq hyps (cddddr hyps))
+	      (setq end-hyp (cl-caddr hyps))
+	      (setq hyp-name (cl-cadddr hyps))
+	      (setq hyps (cl-cddddr hyps))
 	      (if (and (<= start-hyp pos) (<= pos end-hyp))
 		  (progn
 		    (setq found t)
@@ -421,14 +422,14 @@ If no match found, return the empty string."
   (save-excursion
     (let ((pos (point)))
       (beginning-of-line)
-      (block 'loop
+      (cl-block 'loop
 	(while (< (point) pos)
 	  (unless (search-forward-regexp pg-pbrpm-auto-select-regexp nil t)
 	    (return-from 'loop ""))
 	  (if (and (<= (match-beginning 0) pos)
 		   (<= pos (match-end 0)))
-	      (return-from 'loop (match-string 0))))
-	(return-from 'loop "")))))
+	      (cl-return-from 'loop (match-string 0))))
+	(cl-return-from 'loop "")))))
 
 (defun pg-pbrpm-translate-position (buffer pos)
   "If BUFFER is goals-buffer, return POS, otherwise the point in the goal buffer."
diff --git a/generic/pg-user.el b/generic/pg-user.el
index a5ed27a9..57d29f18 100644
--- a/generic/pg-user.el
+++ b/generic/pg-user.el
@@ -558,18 +558,18 @@ last use time, to discourage saving these into the users database."
   (defvar completion-min-length)
   (declare-function add-completion "completion"
                     (string &optional num-uses last-use-time))
-  (mapcar (lambda (cmpl)
-	    ;; completion gives error; trapping is tricky so test again
-	    (if (>= (length cmpl) completion-min-length)
-		(add-completion cmpl -1000 0)))
-	  (proof-ass completion-table)))
+  (when proof-assistant
+    (mapcar (lambda (cmpl)
+	      ;; completion gives error; trapping is tricky so test again
+	      (if (>= (length cmpl) completion-min-length)
+		  (add-completion cmpl -1000 0)))
+	    (proof-ass completion-table))))
 
 ;; NB: completion table is expected to be set when proof-script
 ;; is loaded!  Call `proof-script-add-completions' to update.
 
-(unless (bound-and-true-p byte-compile-current-file) ;FIXME: Yuck!
-  (eval-after-load "completion"
-    '(proof-add-completions)))
+(eval-after-load "completion"
+  '(proof-add-completions))
 
 (defun proof-script-complete (&optional arg)
   "Like `complete' but case-fold-search set to `proof-case-fold-search'."
diff --git a/generic/proof-depends.el b/generic/proof-depends.el
index 9f3b469a..372ce06b 100644
--- a/generic/proof-depends.el
+++ b/generic/proof-depends.el
@@ -241,7 +241,7 @@ This is simply to display the dependency somehow."
 (defun proof-highlight-depcs (name nmspans)
   (let ((helpmsg  (concat "This item is a dependency (ancestor) of " name)))
     (while nmspans
-      (let ((span (cadar nmspans)))
+      (let ((span (cl-cadar nmspans)))
 	(proof-depends-save-old-face span)
 	(span-set-property span 'face 'proof-highlight-dependency-face)
 	;; (span-set-property span 'priority pg-dep-span-priority)
@@ -252,7 +252,7 @@ This is simply to display the dependency somehow."
 (defun proof-highlight-depts (name nmspans)
   (let ((helpmsg  (concat "This item depends on (is a child of) " name)))
     (while nmspans
-      (let ((span (cadar nmspans)))
+      (let ((span (cl-cadar nmspans)))
 	(proof-depends-save-old-face span)
 	(span-set-property span 'face 'proof-highlight-dependent-face)
 	;; (span-set-property span 'priority pg-dep-span-priority)
diff --git a/generic/proof-menu.el b/generic/proof-menu.el
index e43efcc0..dd3d05c8 100644
--- a/generic/proof-menu.el
+++ b/generic/proof-menu.el
@@ -793,7 +793,7 @@ suitable for adding to the proof assistant menu."
   (let*
       ((favs       (proof-ass favourites))
        (rmfavs	   (cl-remove-if
-		    (lambda (f) (string-equal menuname (caddr f)))
+		    (lambda (f) (string-equal menuname (cl-caddr f)))
 		    favs)))
     (unless (equal favs rmfavs)
       (easy-menu-remove-item proof-assistant-menu
@@ -835,7 +835,7 @@ KEY is the optional key binding."
       ((menu-entry (proof-def-favourite command inscript menuname key t))
        (favs       (proof-ass favourites))
        (rmfavs	   (cl-remove-if
-		    (lambda (f) (string-equal menuname (caddr f)))
+		    (lambda (f) (string-equal menuname (cl-caddr f)))
 		    favs))
        (newfavs    (append
 		    rmfavs
@@ -864,11 +864,11 @@ KEY is the optional key binding."
 	      proof-assistant-settings)
 	(dolist (grp (reverse groups))
 	  (let* ((gstgs (cl-mapcan (lambda (stg)
-				  (if (eq (get (car stg) 'pggroup) grp)
-				      (list stg)))
-				proof-assistant-settings))
+				     (if (eq (get (car stg) 'pggroup) grp)
+				         (list stg)))
+				   proof-assistant-settings))
 		 (cmds  (mapcar (lambda (stg)
-				  (apply 'proof-menu-entry-for-setting stg))
+				  (apply #'proof-menu-entry-for-setting stg))
 				(reverse gstgs))))
 	    (setq ents
 		  (if grp (cons (cons grp cmds) ents)
diff --git a/generic/proof-script.el b/generic/proof-script.el
index 4c56fc7b..f8cf0cab 100644
--- a/generic/proof-script.el
+++ b/generic/proof-script.el
@@ -1,4 +1,4 @@
-;;; proof-script.el --- Major mode for proof assistant script files.
+;;; proof-script.el --- Major mode for proof assistant script files.  -*- lexical-binding:t -*-
 
 ;; This file is part of Proof General.
 
@@ -42,6 +42,7 @@
 (declare-function proof-segment-up-to "proof-script")
 (declare-function proof-autosend-enable "pg-user")
 (declare-function proof-interrupt-process "pg-shell")
+(declare-function proof-cd-sync "pg-user" ())
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;
@@ -142,7 +143,7 @@ scripting buffer may have an active queue span.")
 
 ;; ** Getters and setters
 
-(defun proof-span-give-warning (&rest args)
+(defun proof-span-give-warning (&rest _args)
   "Give a warning message.
 Optional argument ARGS is ignored."
   (unless inhibit-read-only
@@ -506,7 +507,7 @@ Intended as a hook function for `proof-shell-handle-error-or-interrupt-hook'."
 (defun pg-clear-script-portions ()
   "Clear record of script portion names and types from internal list."
   (dolist (idtbl pg-script-portions)
-    (maphash (lambda (k span) (span-delete span)) (cdr idtbl))
+    (maphash (lambda (_k span) (span-delete span)) (cdr idtbl))
     (clrhash (cdr idtbl))))
 
 (defun pg-remove-element (idiom id)
@@ -628,14 +629,11 @@ IDIOMSYM is a symbol and ID is a strings."
       (concat "Make "
 	      (if current-prefix-arg "in" "")
 	      "visible all regions of: ")
-      (apply 'vector pg-idioms) nil t))
+      (apply #'vector pg-idioms) nil t))
     current-prefix-arg))
   (let ((elts    (cdr-safe (assq idiom pg-script-portions)))
-	(alterfn (if hide
-		     (lambda (k span)
-		       (pg-set-element-span-invisible span t))
-		   (lambda (k span)
-		     (pg-set-element-span-invisible span nil)))))
+	(alterfn (lambda (_k span)
+		   (pg-set-element-span-invisible span hide))))
     (when elts
       (proof-with-script-buffer ; may be called from menu
        (maphash alterfn elts)))))
@@ -668,7 +666,6 @@ Each span has a 'type property, one of:
     'pbp	  A PBP command inserted automatically into the script."
   (let ((type    (span-property span 'type))
 	(idiom   (span-property span 'idiom))
-	(name    (span-property span 'name))
 	(rawname (span-property span 'rawname)))
     (cond
      (idiom
@@ -1213,10 +1210,10 @@ activation is considered to have failed and an error is given."
       ;; If there's another buffer currently active, we need to
       ;; deactivate it (also fixing up the included files list).
       (when proof-script-buffer
-	    (proof-deactivate-scripting)
-	    ;; Test whether deactivation worked
-	    (if proof-script-buffer
-		(error
+	(proof-deactivate-scripting)
+	;; Test whether deactivation worked
+	(if proof-script-buffer
+	    (error
 	     "You cannot have more than one active scripting buffer!")))
 
       ;; Ensure this buffer is off the included files list.  If we
@@ -1265,21 +1262,21 @@ activation is considered to have failed and an error is given."
       ;; block.  NB: The hook function may send commands to the
       ;; process which will re-enter this function, but should exit
       ;; immediately because scripting has been turned on now.
-      (if proof-activate-scripting-hook
-	  (let
-	      ((activated-interactively	(called-interactively-p 'any)))
-	    (setq proof-shell-last-output-kind nil)
-	    (run-hooks 'proof-activate-scripting-hook)
-	    ;; If activate scripting functions caused an error,
-	    ;; prevent switching to another buffer.  Might be better
-	    ;; to leave to specific instances, or simply run the hooks
-	    ;; as the last step before turning on scripting properly.
-	    (when (or (eq 'error proof-shell-last-output-kind)
-		      (eq 'interrupt proof-shell-last-output-kind))
-	      (proof-deactivate-scripting) ;; turn off again!
-	      ;; Give an error to prevent further actions.
-	      (error
-	       "Scripting not activated because of error or interrupt")))))))
+      (when proof-activate-scripting-hook
+        (defvar activated-interactively)
+	(let ((activated-interactively (called-interactively-p 'any)))
+	  (setq proof-shell-last-output-kind nil)
+	  (run-hooks 'proof-activate-scripting-hook)
+	  ;; If activate scripting functions caused an error,
+	  ;; prevent switching to another buffer.  Might be better
+	  ;; to leave to specific instances, or simply run the hooks
+	  ;; as the last step before turning on scripting properly.
+	  (when (or (eq 'error proof-shell-last-output-kind)
+		    (eq 'interrupt proof-shell-last-output-kind))
+	    (proof-deactivate-scripting) ;; turn off again!
+	    ;; Give an error to prevent further actions.
+	    (error
+	     "Scripting not activated because of error or interrupt")))))))
 
 
 (defun proof-toggle-active-scripting (&optional arg)
@@ -1415,7 +1412,8 @@ Argument SPAN has just been processed."
 						(span-end span)))
       (if (proof-string-match-safe proof-script-evaluate-elisp-comment-regexp str)
 	  (condition-case nil
-	      (eval (car (read-from-string (match-string-no-properties 1 str))))
+	      (eval (car (read-from-string (match-string-no-properties 1 str)))
+                    t)
 	    (t (proof-debug
 		(concat
 		 "lisp error when obeying proof-shell-evaluate-elisp-comment-regexp: \n"
@@ -1599,7 +1597,7 @@ Subroutine of `proof-done-advancing-save'."
       ;; start of the buffer, we make a fake goal-save region.
 
       ;; Delete spans between the previous goal and new command
-      (mapc 'span-delete dels)
+      (mapc #'span-delete dels)
 
       ;; Try to set the name from the goal... [as above]
       (setq nam (or (proof-get-name-from-goal gspan)
@@ -1643,7 +1641,7 @@ Subroutine of `proof-done-advancing-save'."
 ;; command syntax (terminated, not terminated, or lisp-style), whether
 ;; or not PG silently ignores comments, etc.
 
-(defun proof-segment-up-to-parser (pos &optional next-command-end)
+(defun proof-segment-up-to-parser (pos &optional _next-command-end)
   "Parse the script buffer from end of queue/locked region to POS.
 This partitions the script buffer into contiguous regions, classifying
 them by type.  Return a list of lists of the form
@@ -1838,7 +1836,7 @@ The optional QUEUEFLAGS are added to each queue item."
   (let ((start (proof-queue-or-locked-end))
 	(file  (or (buffer-file-name) (buffer-name)))
 	(cb    'proof-done-advancing)
-	span alist semi item end)
+	span alist end)
     (setq semis (nreverse semis))
     (save-match-data
       (dolist (semi semis)
@@ -1927,7 +1925,7 @@ always defaults to inserting a semi (nicer might be to parse for a
 comment, and insert or skip to the next semi)."
   (let ((mrk         (point))
 	(termregexp  (regexp-quote proof-terminal-string))
-	ins incomment nwsp)
+	ins nwsp)
     (if (< mrk (proof-unprocessed-begin))
 	(insert proof-terminal-string) ; insert immediately in locked region
       (if (proof-only-whitespace-to-locked-region-p)
@@ -1953,7 +1951,6 @@ comment, and insert or skip to the next semi)."
 	(unless semis
 	  (error "Can't find a parseable command!"))
 	(when (eq 'unclosed-comment (caar semis))
-	  (setq incomment t)
 	  ;; delete spurious char in comment
 	  (if ins (backward-delete-char 1))
 	  (goto-char mrk)
@@ -2258,17 +2255,22 @@ query saves here."
 ;; Proof General scripting mode definition, part 1.
 ;;
 
+(defvar proof--splash-done nil)
+
 ;;;###autoload
 (define-derived-mode proof-mode fundamental-mode
   proof-general-name
   "Proof General major mode class for proof scripts.
 \\{proof-mode-map}"
 
+  (unless (or proof--splash-done noninteractive)
+    (setq proof--splash-done t)
+    (proof-splash-message))
+
   (setq proof-buffer-type 'script)
 
   ;; Set default indent function (can be overriden in derived modes)
-  (make-local-variable 'indent-line-function)
-  (setq indent-line-function 'proof-indent-line)
+  (setq-local indent-line-function #'proof-indent-line)
 
   ;; During write-file it can happen that we re-set the mode for the
   ;; currently active scripting buffer.  The user might also do this
@@ -2286,9 +2288,9 @@ query saves here."
   (proof-script-set-after-change-functions)
 
   (add-hook 'after-set-visited-file-name-hooks
-	    'proof-script-set-visited-file-name nil t)
+	    #'proof-script-set-visited-file-name nil t)
 
-  (add-hook 'proof-activate-scripting-hook 'proof-cd-sync nil t))
+  (add-hook 'proof-activate-scripting-hook #'proof-cd-sync nil t))
 
 ;; NB: proof-mode-map declared above
 (proof-menu-define-keys proof-mode-map)
@@ -2321,9 +2323,9 @@ This hook also gives a warning in case this is the active scripting buffer."
   "Set the hooks for a proof script buffer.
 The hooks set here are cleared by `write-file', so we use this function
 to restore them using `after-set-visited-file-name-hooks'."
-  (add-hook 'kill-buffer-hook 'proof-script-kill-buffer-fn t t)
+  (add-hook 'kill-buffer-hook #'proof-script-kill-buffer-fn t t)
   ;; Reverting buffer is same as killing it as far as PG is concerned
-  (add-hook 'before-revert-hook 'proof-script-kill-buffer-fn t t))
+  (add-hook 'before-revert-hook #'proof-script-kill-buffer-fn t t))
 
 (defun proof-script-kill-buffer-fn ()
   "Value of `kill-buffer-hook' for proof script buffers.
@@ -2616,17 +2618,17 @@ finish setup which depends on specific proof assistant configuration."
   "Choose parsing mechanism according to different kinds of script syntax.
 Choice of function depends on configuration setting."
   (unless (fboundp 'proof-segment-up-to)
-    (defalias 'proof-segment-up-to 'proof-segment-up-to-parser)
+    (defalias 'proof-segment-up-to #'proof-segment-up-to-parser)
     (cond
      (proof-script-parse-function
       ;; already set, nothing to do
       )
      (proof-script-sexp-commands
-      (setq proof-script-parse-function 'proof-script-generic-parse-sexp))
+      (setq proof-script-parse-function #'proof-script-generic-parse-sexp))
      (proof-script-command-start-regexp
-      (setq proof-script-parse-function 'proof-script-generic-parse-cmdstart))
+      (setq proof-script-parse-function #'proof-script-generic-parse-cmdstart))
      ((or proof-script-command-end-regexp proof-terminal-string)
-      (setq  proof-script-parse-function 'proof-script-generic-parse-cmdend)
+      (setq  proof-script-parse-function #'proof-script-generic-parse-cmdend)
       (unless proof-script-command-end-regexp
 	(proof-warn-if-unset "probof-config-done" 'proof-terminal-string)
 	(setq proof-script-command-end-regexp
@@ -2726,7 +2728,7 @@ Stores recent results of `proof-segment-up-to' in reverse order.")
 		  (cdr semis))))
       usedsemis)))
 
-(defun proof-script-after-change-function (start end prelength)
+(defun proof-script-after-change-function (start _end _prelength)
   "Value for `after-change-functions' in proof script buffers."
   (setq proof-last-edited-low-watermark
 	(min (or proof-last-edited-low-watermark (point-max))
@@ -2741,7 +2743,7 @@ Stores recent results of `proof-segment-up-to' in reverse order.")
 (defun proof-script-set-after-change-functions ()
   "Set `after-change-functions' for script buffers."
   (add-hook 'after-change-functions
-	    'proof-script-after-change-function nil t))
+	    #'proof-script-after-change-function nil t))
 
 
 
diff --git a/generic/proof-splash.el b/generic/proof-splash.el
index 75164890..600e9b4e 100644
--- a/generic/proof-splash.el
+++ b/generic/proof-splash.el
@@ -3,7 +3,7 @@
 ;; This file is part of Proof General.
 
 ;; Portions © Copyright 1994-2012  David Aspinall and University of Edinburgh
-;; Portions © Copyright 2003, 2012, 2014  Free Software Foundation, Inc.
+;; Portions © Copyright 2003-2018  Free Software Foundation, Inc.
 ;; Portions © Copyright 2001-2017  Pierre Courtieu
 ;; Portions © Copyright 2010, 2016  Erik Martin-Dorel
 ;; Portions © Copyright 2011-2013, 2016-2017  Hendrik Tews
@@ -270,7 +270,7 @@ binding to remove this buffer."
 (defun proof-splash-message ()
   "Make sure the user gets welcomed one way or another."
   (interactive)
-  (unless (or proof-splash-seen noninteractive (bound-and-true-p byte-compile-current-file))
+  (unless (or proof-splash-seen noninteractive)
     (if proof-splash-enable
 	(progn
 	  ;; disable ordinary emacs splash
diff --git a/generic/proof-syntax.el b/generic/proof-syntax.el
index e93f5ca4..d494279a 100644
--- a/generic/proof-syntax.el
+++ b/generic/proof-syntax.el
@@ -36,18 +36,14 @@ Uses a regexp of the form \\_<...\\_>."
 (defconst proof-no-regexp "\\<\\>"
   "A regular expression that never matches anything.")
 
-(defsubst proof-regexp-alt (&rest args)
+(defsubst proof-regexp-alt-list (args)
   "Return the regexp which matches any of the regexps ARGS."
-  ;; see regexp-opt (NB: but that is for strings, not regexps)
-  (let ((res ""))
-    (dolist (regexp args)
-      (setq res (concat res (if (string-equal res "") "\\(?:" "\\|\\(?:")
-			regexp "\\)")))
-    res))
+  (mapconcat #'identity args "\\|"))
 
-(defsubst proof-regexp-alt-list (args)
+(defsubst proof-regexp-alt (&rest args)
   "Return the regexp which matches any of the regexps ARGS."
-  (apply 'proof-regexp-alt args))
+  ;; see regexp-opt (NB: but that is for strings, not regexps)
+  (proof-regexp-alt-list args))
 
 (defsubst proof-re-search-forward-region (startre endre)
   "Search for a region delimited by regexps STARTRE and ENDRE.
diff --git a/generic/proof-useropts.el b/generic/proof-useropts.el
index 9a60e0ac..4ce51c99 100644
--- a/generic/proof-useropts.el
+++ b/generic/proof-useropts.el
@@ -3,7 +3,7 @@
 ;; This file is part of Proof General.
 
 ;; Portions © Copyright 1994-2012  David Aspinall and University of Edinburgh
-;; Portions © Copyright 2003, 2012, 2014  Free Software Foundation, Inc.
+;; Portions © Copyright 2003-2018  Free Software Foundation, Inc.
 ;; Portions © Copyright 2001-2017  Pierre Courtieu
 ;; Portions © Copyright 2010, 2016  Erik Martin-Dorel
 ;; Portions © Copyright 2011-2013, 2016-2017  Hendrik Tews
@@ -50,7 +50,7 @@ approximation we test whether proof-config is fully-loaded yet."
   (set-default sym value)
   (when (and
 	 (not noninteractive)
-	 (not (bound-and-true-p byte-compile-current-file))
+	 (not (bound-and-true-p byte-compile-current-file)) ;FIXME: Yuck!
 	 (featurep 'pg-custom)
 	 (featurep 'proof-config))
       (if (fboundp sym)
diff --git a/generic/proof-utils.el b/generic/proof-utils.el
index 99e537c5..4a15301a 100644
--- a/generic/proof-utils.el
+++ b/generic/proof-utils.el
@@ -23,6 +23,7 @@
 
 ;;; Code:
 
+(eval-when-compile (require 'cl-lib))
 ;;
 ;; Give Emacs version mismatch error here.
 ;;
@@ -58,8 +59,6 @@
 (require 'proof-autoloads)		; interface fns
 (require 'scomint)			; for proof-shell-live-buffer
 
-;;; Code:
-
 ;;
 ;; Handy macros
 ;;
@@ -247,7 +246,8 @@ Experimentally we display a message from time to time advertising
   ;; IF there *isn't* a visible window showing buffer...
   (unless (get-buffer-window buffer 0)
     (if proof-three-window-enable
-        (if (< proof-advertise-layout-count 30) (incf proof-advertise-layout-count)
+        (if (< proof-advertise-layout-count 30)
+            (cl-incf proof-advertise-layout-count)
           (message (substitute-command-keys "Hit \\[proof-layout-windows] to reset layout"))
           (setq proof-advertise-layout-count 0)))
     ;; THEN either we are in 2 wins mode and we must switch the assoc
@@ -589,25 +589,23 @@ The name of the defined function is returned."
   `(proof-deffloatset-fn (quote ,var) (quote ,othername)))
 
 (defun proof-defstringset-fn (var &optional othername)
-  "Define a function <VAR>-toggle for setting an integer customize setting VAR.
-Args as for the macro `proof-defstringset', except will be evaluated."
+  "Define a function OTHERNAME for setting an string customize setting VAR.
+OTHERNAME defaults to `VAR-stringset'."
   (eval
-   `(defun ,(if othername othername
-	      (intern (concat (symbol-name var) "-stringset"))) (arg)
-	      ,(concat "Set `" (symbol-name var) "' to ARG.
-This function simply uses customize-set-variable to set the variable.
+   `(defun ,(or othername
+	        (intern (concat (symbol-name var) "-stringset")))
+        (arg)
+      ,(concat "Set `" (symbol-name var) "' to ARG.
+This function simply uses `customize-set-variable' to set the variable.
 It was constructed with `proof-defstringset-fn'.")
-	      (interactive ,(format "sValue for %s (a string): "
-				    (symbol-name var)))
-	      (customize-set-variable (quote ,var) arg))))
-
-(defmacro proof-defstringset (var &optional othername)
-  "The setting function uses customize-set-variable to change the variable.
-OTHERNAME gives an alternative name than the default <VAR>-stringset.
-The name of the defined function is returned."
-  `(proof-defstringset-fn (quote ,var) (quote ,othername)))
-
-
+      (interactive (list
+		    (read-string
+		     (format "Value for %s (default %s): "
+			     (symbol-name (quote ,var))
+			     (symbol-value (quote ,var)))
+                     nil nil
+		     (symbol-value (quote ,var)))))
+      (customize-set-variable (quote ,var) arg))))
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;;
diff --git a/generic/proof.el b/generic/proof.el
index f3b3b276..769459df 100644
--- a/generic/proof.el
+++ b/generic/proof.el
@@ -1,4 +1,4 @@
-;;; proof.el --- Proof General theorem prover interface
+;;; proof.el --- Proof General theorem prover interface  -*- lexical-binding:t -*-
 
 ;; This file is part of Proof General.
 
@@ -33,9 +33,6 @@
 
 (require 'proof-site)			; site/prover config, global vars, autoloads
 
-(unless (or noninteractive (bound-and-true-p byte-compile-current-file))
-  (proof-splash-message))		; welcome the user now.
-
 (require 'proof-utils)			; utilities
 (require 'proof-config)			; configuration variables
 (require 'proof-auxmodes)		; auxmode functions
diff --git a/lib/maths-menu.el b/lib/maths-menu.el
index 32911a35..43592bed 100644
--- a/lib/maths-menu.el
+++ b/lib/maths-menu.el
@@ -1,13 +1,13 @@
-;;; maths-menu.el --- insert maths characters from a menu  -*-coding: iso-2022-7bit;-*-
+;;; maths-menu.el --- insert maths characters from a menu  -*- lexical-binding:t; coding: utf-8 -*-
 
 ;; This file is part of Proof General.
 
-;; Portions ,A)(B Copyright 1994-2012  David Aspinall and University of Edinburgh
-;; Portions ,A)(B Copyright 2003, 2012, 2014  Free Software Foundation, Inc.
-;; Portions ,A)(B Copyright 2001-2017  Pierre Courtieu
-;; Portions ,A)(B Copyright 2010, 2016  Erik Martin-Dorel
-;; Portions ,A)(B Copyright 2011-2013, 2016-2017  Hendrik Tews
-;; Portions ,A)(B Copyright 2015-2017  Cl,Ai(Bment Pit-Claudel
+;; Portions © Copyright 1994-2012  David Aspinall and University of Edinburgh
+;; Portions © Copyright 2003-2018  Free Software Foundation, Inc.
+;; Portions © Copyright 2001-2017  Pierre Courtieu
+;; Portions © Copyright 2010, 2016  Erik Martin-Dorel
+;; Portions © Copyright 2011-2013, 2016-2017  Hendrik Tews
+;; Portions © Copyright 2015-2017  Clément Pit-Claudel
 
 ;; Author: Dave Love <fx@gnu.org>
 ;; Keywords: convenience
@@ -86,262 +86,262 @@
 (defvar maths-menu-menu
   (maths-menu-build-menu
    '(("Logic"
-      (?$A!D(B "and")
-      (?$A!E(B "or")
-      (?$,1x (B "for all")
-      (?$,1x#(B "there exists")
-      (?$,1x$(B "there does not exist")
-      (?$,1yd(B "down tack")
-      (?$,1ye(B "up tack"))
+      (?∧ "and")
+      (?∨ "or")
+      (?∀ "for all")
+      (?∃ "there exists")
+      (?∄ "there does not exist")
+      (?⊤ "down tack")
+      (?⊥ "up tack"))
      ("Binops 1"
-      (?,A1(B "plus-minus sign")
-      (?$,1x3(B "minus-or-plus sign")
-      (?,AW(B "multiplication sign")
-      (?,Aw(B "division sign")
-      (?$,1x2(B "minus sign")
-      (?$,1x7(B "asterisk operator")
-      (?$,1z&(B "star operator")
-      (?$,2"+(B "white circle")
-      (?$,1s"(B "bullet")
-      (?,A7(B "middle dot")
-      (?$,1xI(B "intersection")
-      (?$,1xJ(B "union")
-      (?$,1yN(B "multiset union")
-      (?$,1yS(B "square cap")
-      (?$,1yT(B "square cup")
-      (?$,1xH(B "logical or")
-      (?$,1xG(B "logical and")
-      (?$,1x6(B "set minus")
-      (?$,1x`(B "wreath product"))
+      (?± "plus-minus sign")
+      (?∓ "minus-or-plus sign")
+      (?× "multiplication sign")
+      (?÷ "division sign")
+      (?− "minus sign")
+      (?∗ "asterisk operator")
+      (?⋆ "star operator")
+      (?○ "white circle")
+      (?• "bullet")
+      (?· "middle dot")
+      (?∩ "intersection")
+      (?∪ "union")
+      (?⊎ "multiset union")
+      (?⊓ "square cap")
+      (?⊔ "square cup")
+      (?∨ "logical or")
+      (?∧ "logical and")
+      (?∖ "set minus")
+      (?≀ "wreath product"))
      ("Binops 2"
-      (?$,1z$(B "diamond operator")
-      (?$,2!s(B "white up-pointing triangle")
-      (?$,2!}(B "white down-pointing triangle")
-      (?$,2"#(B "white left-pointing small triangle")
-      (?$,2!y(B "white right-pointing small triangle")
-      (?$,2"!(B "white left-pointing triangle")
-      (?$,2!w(B "white right-pointing triangle")
-      (?$,1yU(B "circled plus")
-      (?$,1yV(B "circled minus")
-      (?$,1yW(B "circled times")
-      (?$,1yX(B "circled division slash")
-      (?$,1yY(B "circled dot operator")
-      (?$,2"O(B "large circle")
-      (?$,1s (B "dagger")
-      (?$,1s!(B "double dagger")
-      (?$,1yt(B "normal subgroup of or equal to")
-      (?$,1yu(B "contains as normal subgroup or equal to"))
+      (?⋄ "diamond operator")
+      (?△ "white up-pointing triangle")
+      (?▽ "white down-pointing triangle")
+      (?◃ "white left-pointing small triangle")
+      (?▹ "white right-pointing small triangle")
+      (?◁ "white left-pointing triangle")
+      (?▷ "white right-pointing triangle")
+      (?⊕ "circled plus")
+      (?⊖ "circled minus")
+      (?⊗ "circled times")
+      (?⊘ "circled division slash")
+      (?⊙ "circled dot operator")
+      (?◯ "large circle")
+      (?† "dagger")
+      (?‡ "double dagger")
+      (?⊴ "normal subgroup of or equal to")
+      (?⊵ "contains as normal subgroup or equal to"))
      ("Relations 1"
-      (?$,1y$(B "less-than or equal to")
-      (?$,1y:(B "precedes")
-      (?$,1y*(B "much less-than")
-      (?$,1yB(B "subset of")
-      (?$,1yF(B "subset of or equal to")
-      (?$,1yO(B "square image of")
-      (?$,1yQ(B "square image of or equal to")
-      (?$,1x((B "element of")
-      (?$,1x)(B "not an element of")
-      (?$,1yb(B "right tack")
-      (?$,1y%(B "greater-than or equal to")
-      (?$,1y;(B "succeeds")
-      (?$,1y=(B "succeeds or equal to")
-      (?$,1y+(B "much greater-than")
-      (?$,1yC(B "superset of")
-      (?$,1yG(B "superset of or equal to")
-      (?$,1yP(B "square original of")
-      (?$,1yR(B "square original of or equal to")
-      (?$,1x+(B "contains as member")
-      (?$,1y!(B "identical to")
-      (?$,1y"(B "not identical to") )
+      (?≤ "less-than or equal to")
+      (?≺ "precedes")
+      (?≪ "much less-than")
+      (?⊂ "subset of")
+      (?⊆ "subset of or equal to")
+      (?⊏ "square image of")
+      (?⊑ "square image of or equal to")
+      (?∈ "element of")
+      (?∉ "not an element of")
+      (?⊢ "right tack")
+      (?≥ "greater-than or equal to")
+      (?≻ "succeeds")
+      (?≽ "succeeds or equal to")
+      (?≫ "much greater-than")
+      (?⊃ "superset of")
+      (?⊇ "superset of or equal to")
+      (?⊐ "square original of")
+      (?⊒ "square original of or equal to")
+      (?∋ "contains as member")
+      (?≡ "identical to")
+      (?≢ "not identical to") )
      ("Relations 2"
-      (?$,1yc(B "left tack")
-      (?$,1x\(B "tilde operator")
-      (?$,1xc(B "asymptotically equal to")
-      (?$,1xm(B "equivalent to")
-      (?$,1xh(B "almost equal to")
-      (?$,1xe(B "approximately equal to")
-      (?$,1y (B "not equal to")
-      (?$,1xp(B "approaches the limit")
-      (?$,1x=(B "proportional to")
-      (?$,1yg(B "models")
-      (?$,1xC(B "divides")
-      (?$,1xE(B "parallel to")
-      (?$,1z((B "bowtie")
-      (?$,1z((B "bowtie")
-      (?$,1{#(B "smile")
-      (?$,1{"(B "frown")
-      (?$,1xy(B "estimates")
-      (?$,1z_(B "z notation bag membership"))
+      (?⊣ "left tack")
+      (?∼ "tilde operator")
+      (?≃ "asymptotically equal to")
+      (?≍ "equivalent to")
+      (?≈ "almost equal to")
+      (?≅ "approximately equal to")
+      (?≠ "not equal to")
+      (?≐ "approaches the limit")
+      (?∝ "proportional to")
+      (?⊧ "models")
+      (?∣ "divides")
+      (?∥ "parallel to")
+      (?⋈ "bowtie")
+      (?⋈ "bowtie")
+      (?⌣ "smile")
+      (?⌢ "frown")
+      (?≙ "estimates")
+      (?⋿ "z notation bag membership"))
      ("Arrows"
-      (?$,1vp(B "leftwards arrow")
-      (?$,1wP(B "leftwards double arrow")
-      (?$,1vr(B "rightwards arrow")
-      (?$,1wR(B "rightwards double arrow")
-      (?$,1vt(B "left right arrow")
-      (?$,1wT(B "left right double arrow")
-      (?$,1w&(B "rightwards arrow from bar")
-      (?$,1w)(B "leftwards arrow with hook")
-      (?$,1w<(B "leftwards harpoon with barb upwards")
-      (?$,1w=(B "leftwards harpoon with barb downwards")
-      (?$,1wL(B "rightwards harpoon over leftwards harpoon")
-      (?$,1w&(B "rightwards arrow from bar")
-      (?$,1w*(B "rightwards arrow with hook")
-      (?$,1w@(B "rightwards harpoon with barb upwards")
-      (?$,1wA(B "rightwards harpoon with barb downwards")
-      (?$,1v}(B "rightwards wave arrow")
-      (?$,1vq(B "upwards arrow")
-      (?$,1wQ(B "upwards double arrow")
-      (?$,1vs(B "downwards arrow")
-      (?$,1wS(B "downwards double arrow")
-      (?$,1vu(B "up down arrow")
-      (?$,1vw(B "north east arrow")
-      (?$,1vx(B "south east arrow")
-      (?$,1vy(B "south west arrow")
-      (?$,1vv(B "north west arrow")
-      (?$,1w[(B "rightwards triple arrow"))
+      (?← "leftwards arrow")
+      (?⇐ "leftwards double arrow")
+      (?→ "rightwards arrow")
+      (?⇒ "rightwards double arrow")
+      (?↔ "left right arrow")
+      (?⇔ "left right double arrow")
+      (?↦ "rightwards arrow from bar")
+      (?↩ "leftwards arrow with hook")
+      (?↼ "leftwards harpoon with barb upwards")
+      (?↽ "leftwards harpoon with barb downwards")
+      (?⇌ "rightwards harpoon over leftwards harpoon")
+      (?↦ "rightwards arrow from bar")
+      (?↪ "rightwards arrow with hook")
+      (?⇀ "rightwards harpoon with barb upwards")
+      (?⇁ "rightwards harpoon with barb downwards")
+      (?↝ "rightwards wave arrow")
+      (?↑ "upwards arrow")
+      (?⇑ "upwards double arrow")
+      (?↓ "downwards arrow")
+      (?⇓ "downwards double arrow")
+      (?↕ "up down arrow")
+      (?↗ "north east arrow")
+      (?↘ "south east arrow")
+      (?↙ "south west arrow")
+      (?↖ "north west arrow")
+      (?⇛ "rightwards triple arrow"))
      ("Long arrows"
-      (?$,2'v(B "long rightwards arrow")
-      (?$,2'w(B "long left right arrow")
-      (?$,2'x(B "long left double arrow")
-      (?$,2'y(B "long right double arrow")
-      (?$,2'z(B "long left right double arrow")
-      (?$,2'{(B "long left arrow from bar")
-      (?$,2'|(B "long right arrow from bar")
-      (?$,2'}(B "long left double arrow bar")
-      (?$,2'~(B "long right double arrow from bar")
-      (?$,2'(B "long rightwards squiggle arrow"))
+      (?⟶ "long rightwards arrow")
+      (?⟷ "long left right arrow")
+      (?⟸ "long left double arrow")
+      (?⟹ "long right double arrow")
+      (?⟺ "long left right double arrow")
+      (?⟻ "long left arrow from bar")
+      (?⟼ "long right arrow from bar")
+      (?⟽ "long left double arrow bar")
+      (?⟾ "long right double arrow from bar")
+      (?⟿ "long rightwards squiggle arrow"))
      ("Symbols 1"
-      (?$,1uu(B "alef symbol") ; don't use letter alef (avoid bidi confusion)
-      (?$,1uO(B "planck constant over two pi")
-      (?$,1 Q(B "latin small letter dotless i")
-      (?$,1uS(B "script small l")
-      (?$,1uX(B "script capital p")
-      (?$,1u\(B "black-letter capital r")
-      (?$,1uQ(B "black-letter capital i")
-      (?$,1ug(B "inverted ohm sign")
-      (?$,1s2(B "prime")
-      (?$,1x%(B "empty set")
-      (?$,1x'(B "nabla")
-      (?$,1x:(B "square root")
-      (?$,1x;(B "cube root")
-      (?$,1x@(B "angle")
-      (?,A,(B "not sign")
-      (?$,2#o(B "music sharp sign")
-      (?$,1x"(B "partial differential")
-      (?$,1x>(B "infinity") )
+      (?ℵ "alef symbol") ; don't use letter alef (avoid bidi confusion)
+      (?ℏ "planck constant over two pi")
+      (?ı "latin small letter dotless i")
+      (?ℓ "script small l")
+      (?℘ "script capital p")
+      (?ℜ "black-letter capital r")
+      (?ℑ "black-letter capital i")
+      (?℧ "inverted ohm sign")
+      (?′ "prime")
+      (?∅ "empty set")
+      (?∇ "nabla")
+      (?√ "square root")
+      (?∛ "cube root")
+      (?∠ "angle")
+      (?¬ "not sign")
+      (?♯ "music sharp sign")
+      (?∂ "partial differential")
+      (?∞ "infinity") )
      ("Symbols 2"
-      (?$,2!a(B "white square")
-      (?$,2"'(B "white diamond")
-      (?$,2!u(B "white up-pointing small triangle")
-      (?$,1x1(B "n-ary summation")
-      (?$,1x/(B "n-ary product")
-      (?$,1x0(B "n-ary coproduct")
-      (?$,1xK(B "integral")
-      (?$,1xN(B "contour integral")
-      (?$,1z"(B "n-ary intersection")
-      (?$,1z#(B "n-ary union")
-      (?$,1z!(B "n-ary logical or")
-      (?$,1z (B "n-ary logical and")
-      (?$,1uU(B "double-struck capital n")
-      (?$,1uY(B "double-struck capital p")
-      (?$,1uZ(B "double-struck capital q")
-      (?$,1u](B "double-struck capital r")
-      (?$,1ud(B "double-struck capital z")
-      (?$,1uP(B "script capital i")
-      (?$,1![(B "latin small letter lambda with stroke")
-      (?$,1xT(B "therefore")
-      (?$,1s&(B "horizontal ellipsis")
-      (?$,1zO(B "midline horizontal ellipsis")
-      (?$,1zN(B "vertical ellipsis")
-      (?$,1zQ(B "down right diagonal ellipsis")
-      (?$,1zP(B "up right diagonal ellipsis")
-      (?$,2,!(B "z notation spot")
-      (?$,2,"(B "z notation type colon"))
+      (?□ "white square")
+      (?◇ "white diamond")
+      (?▵ "white up-pointing small triangle")
+      (?∑ "n-ary summation")
+      (?∏ "n-ary product")
+      (?∐ "n-ary coproduct")
+      (?∫ "integral")
+      (?∮ "contour integral")
+      (?⋂ "n-ary intersection")
+      (?⋃ "n-ary union")
+      (?⋁ "n-ary logical or")
+      (?⋀ "n-ary logical and")
+      (?ℕ "double-struck capital n")
+      (?ℙ "double-struck capital p")
+      (?ℚ "double-struck capital q")
+      (?ℝ "double-struck capital r")
+      (?ℤ "double-struck capital z")
+      (?ℐ "script capital i")
+      (?ƛ "latin small letter lambda with stroke")
+      (?∴ "therefore")
+      (?… "horizontal ellipsis")
+      (?⋯ "midline horizontal ellipsis")
+      (?⋮ "vertical ellipsis")
+      (?⋱ "down right diagonal ellipsis")
+      (?⋰ "up right diagonal ellipsis")
+      (?⦁ "z notation spot")
+      (?⦂ "z notation type colon"))
      ("Delimiters"
-      (?\$,1zj(B "left floor")
-      (?\$,1zh(B "left ceiling")
-      (?\$,1{)(B "left-pointing angle bracket")
-      (?\$,1zk(B "right floor")
-      (?\$,1zi(B "right ceiling")
-      (?\$,1{*(B "right-pointing angle bracket")
-      (?\$,2=Z(B "left white square bracket")
-      (?\$,2=[(B "right white square bracket")
-      (?\$,2=J(B "left double angle bracket")
-      (?\$,2=K(B "right double angle bracket")
-      (?\$,2,'(B "z notation left image bracket")
-      (?\$,2,((B "z notation right image bracket")
-      (?\$,2,)(B "z notation left binding bracket")
-      (?\$,2,*(B "z notation right binding bracket"))
+      (?\⌊ "left floor")
+      (?\⌈ "left ceiling")
+      (?\〈 "left-pointing angle bracket")
+      (?\⌋ "right floor")
+      (?\⌉ "right ceiling")
+      (?\〉 "right-pointing angle bracket")
+      (?\〚 "left white square bracket")
+      (?\〛 "right white square bracket")
+      (?\《 "left double angle bracket")
+      (?\》 "right double angle bracket")
+      (?\⦇ "z notation left image bracket")
+      (?\⦈ "z notation right image bracket")
+      (?\⦉ "z notation left binding bracket")
+      (?\⦊ "z notation right binding bracket"))
      ("Greek LC"
-      (?$,1'1(B "alpha")
-      (?$,1'2(B "beta")
-      (?$,1'3(B "gamma")
-      (?$,1'4(B "delta")
-      (?$,1'5(B "epsilon")
-      (?$,1'6(B "zeta")
-      (?$,1'7(B "eta")
-      (?$,1'8(B "theta")
-      (?$,1'Q(B "theta symbol")
-      (?$,1'9(B "iota")
-      (?$,1':(B "kappa")
-      (?$,1';(B "lamda")
-      (?$,1'<(B "mu")
-      (?$,1'=(B "nu")
-      (?$,1'>(B "xi")
-      (?$,1'@(B "pi")
-      (?$,1'V(B "pi symbol")
-      (?$,1'A(B "rho")
-      (?$,1'q(B "rho symbol")
-      (?$,1'C(B "sigma")
-      (?$,1'B(B "final sigma")
-      (?$,1'D(B "tau")
-      (?$,1'E(B "upsilon")
-      (?$,1'F(B "phi")
-      (?$,1'U(B "phi symbol")
-      (?$,1'G(B "chi")
-      (?$,1'H(B "psi")
-      (?$,1'I(B "omega"))
+      (?α "alpha")
+      (?β "beta")
+      (?γ "gamma")
+      (?δ "delta")
+      (?ε "epsilon")
+      (?ζ "zeta")
+      (?η "eta")
+      (?θ "theta")
+      (?ϑ "theta symbol")
+      (?ι "iota")
+      (?κ "kappa")
+      (?λ "lamda")
+      (?μ "mu")
+      (?ν "nu")
+      (?ξ "xi")
+      (?π "pi")
+      (?ϖ "pi symbol")
+      (?ρ "rho")
+      (?ϱ "rho symbol")
+      (?σ "sigma")
+      (?ς "final sigma")
+      (?τ "tau")
+      (?υ "upsilon")
+      (?φ "phi")
+      (?ϕ "phi symbol")
+      (?χ "chi")
+      (?ψ "psi")
+      (?ω "omega"))
      ("Greek UC"
-      (?$,1&s(B "Gamma")
-      (?$,1&t(B "Delta")
-      (?$,1&x(B "Theta")
-      (?$,1&{(B "Lamda")
-      (?$,1&~(B "Xi")
-      (?$,1' (B "Pi")
-      (?$,1'#(B "Sigma")
-      (?$,1'%(B "Upsilon")
-      (?$,1'&(B "Phi")
-      (?$,1'((B "Psi")
-      (?$,1')(B "Omega"))
+      (?Γ "Gamma")
+      (?Δ "Delta")
+      (?Θ "Theta")
+      (?Λ "Lamda")
+      (?Ξ "Xi")
+      (?Π "Pi")
+      (?Σ "Sigma")
+      (?Υ "Upsilon")
+      (?Φ "Phi")
+      (?Ψ "Psi")
+      (?Ω "Omega"))
      ("Sub/super"
-      (?$,1s}(B "superscript left parenthesis")
-      (?$,1s~(B "superscript right parenthesis")
-      (?$,1sz(B "superscript plus sign")
-      (?$,1s{(B "superscript minus")
-      (?$,1sp(B "superscript zero")
-      (?,A9(B "superscript one")
-      (?,A2(B "superscript two")
-      (?,A3(B "superscript three")
-      (?$,1st(B "superscript four")
-      (?$,1su(B "superscript five")
-      (?$,1sv(B "superscript six")
-      (?$,1sw(B "superscript seven")
-      (?$,1sx(B "superscript eight")
-      (?$,1sy(B "superscript nine")
-      (?$,1t-(B "subscript left parenthesis")
-      (?$,1t.(B "subscript right parenthesis")
-      (?$,1t*(B "subscript plus sign")
-      (?$,1t+(B "subscript minus")
-      (?$,1t (B "subscript zero")
-      (?$,1t!(B "subscript one")
-      (?$,1t"(B "subscript two")
-      (?$,1t#(B "subscript three")
-      (?$,1t$(B "subscript four")
-      (?$,1t%(B "subscript five")
-      (?$,1t&(B "subscript six")
-      (?$,1t'(B "subscript seven")
-      (?$,1t((B "subscript eight")
-      (?$,1t)(B "subscript nine")))))
+      (?⁽ "superscript left parenthesis")
+      (?⁾ "superscript right parenthesis")
+      (?⁺ "superscript plus sign")
+      (?⁻ "superscript minus")
+      (?⁰ "superscript zero")
+      (?¹ "superscript one")
+      (?² "superscript two")
+      (?³ "superscript three")
+      (?⁴ "superscript four")
+      (?⁵ "superscript five")
+      (?⁶ "superscript six")
+      (?⁷ "superscript seven")
+      (?⁸ "superscript eight")
+      (?⁹ "superscript nine")
+      (?₍ "subscript left parenthesis")
+      (?₎ "subscript right parenthesis")
+      (?₊ "subscript plus sign")
+      (?₋ "subscript minus")
+      (?₀ "subscript zero")
+      (?₁ "subscript one")
+      (?₂ "subscript two")
+      (?₃ "subscript three")
+      (?₄ "subscript four")
+      (?₅ "subscript five")
+      (?₆ "subscript six")
+      (?₇ "subscript seven")
+      (?₈ "subscript eight")
+      (?₉ "subscript nine")))))
 
 (defvar maths-menu-mode-map
   (let ((map (make-sparse-keymap)))
diff --git a/obsolete/plastic/plastic.el b/obsolete/plastic/plastic.el
index cf69a731..39f6c01f 100644
--- a/obsolete/plastic/plastic.el
+++ b/obsolete/plastic/plastic.el
@@ -546,8 +546,8 @@ For Plastic, we assume that module identifiers coincide with file names."
 		      (aset string i ?\ )
 		      (cl-incf i) )))
 	(keep-rest (lambda ()
-		     (loop for x in (string-to-list plastic-lit-string)
-		       do (aset string i ?\ ) (cl-incf i))
+		     (cl-loop for x in (string-to-list plastic-lit-string)
+		              do (aset string i ?\ ) (cl-incf i))
 		     (while (and (< i l)
 				 (/= (aref string i) ?\n)
 				 (/= (aref string i) ?-))
diff --git a/phox/phox.el b/phox/phox.el
index 5c5674ed..375272de 100644
--- a/phox/phox.el
+++ b/phox/phox.el
@@ -27,15 +27,15 @@
  proof-script-comment-start	"(*"
  proof-script-comment-end	"*)"
  proof-script-syntax-table-entries
-   '(?( "()1"
-     ?) ")(4"
+   '(?\( "()1"
+     ?\) ")(4"
      ?* ". 23"
      ?$ "w"
      ?_ "w"
      ?. "w")
  proof-shell-syntax-table-entries
-   '(?( "()1"
-     ?) ")(4"
+   '(?\( "()1"
+     ?\) ")(4"
      ?* ". 23"
      ?$ "w"
      ?_ "w"