Cosmetic cleanup of coq-smie, coq-syntax, and coq-abbrev.

Fix a few more cl.el leftovers.  Get rid of remaining use of iso-2022.
Use SMIE unconditionally.

* coq/coq-abbrev.el: Use lexical-binding.
(coq-install-abbrevs): Delete, only keep the relevant contents.
(proof-defstringset-fn): Remove.  Fold changes into the main version.

* coq/coq-indent.el (coq-find-real-start): Use forward-comment.

* coq/coq-smie.el: Use lexical-binding.  Assume `smie` is available.
(coq--string-suffix-p): Rename from coq-string-suffix-p.
Use string-suffix-p for it when available.
(string-suffix-p): Never define here.  Change all users to use
coq--string-suffix-p instead.
(coq-smie-.-deambiguate): Use forward-comment.  Remove unused var `beg`.
(coq-backward-token-fast-nogluing-dot-friends)
(coq-forward-token-fast-nogluing-dot-friends): Remove unused var
`tok-other`.
(coq-smie-search-token-backward): Remove unused var `p`.
(coq-smie-:=-deambiguate, coq-smie-backward-token): Prefer char-before
over looking-back.
(coq-smie-rules): Use `pcase` over deprecated cl's `case`.

* coq/coq-syntax.el: Use lexical-binding.
(coq-count-match): Rewrite so it doesn't do needless heap-allocation.
(coq-module-opening-p, coq-section-command-p, coq-goal-command-str-p):
Use case-fold-search rather than proof-string-match.
(coq-goal-command-regexp): Forward-declare.
(coq-save-command-regexp-strict): Move before first use.
(coq-reserved-regexp): Use a single \_< ... \_>.
(coq-detect-hyps-positions): Limit search for looking-back.

* coq/coq.el: Remove SMIE declarations since SMIE is always used.
(coq-use-smie): Remove, unused.
(coq-smie): Always require.

* generic/pg-pbrpm.el: Fix leftover cl.el uses.

* generic/proof-utils.el (proof-defstringset-fn): Fix copy&paste error
in the docstring, improve interactive prompt.

* lib/maths-menu.el: Use utf-8 and lexical-binding.

10 files changed, 530 insertions, 579 deletions

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-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-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 e1a9a7e3..7a11a43f 100644
--- a/coq/coq-syntax.el
+++ b/coq/coq-syntax.el
@@ -1,4 +1,4 @@
-;;; 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.
 
@@ -987,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 "")))
+  (let ((nbmatch 0) (pos 0) (end (length str))
+        (case-fold-search nil))
+    (while (and (< pos end)
+                (string-match regexp str pos))
       (cl-incf nbmatch)
-      (if (= (match-end 0) 0) (setq str (substring str 1))
-        (setq str (substring str (match-end 0)))))
+      (setq pos (max (match-end 0) (1+ pos))))
     nbmatch))
 
 ;; Module and or section openings are detected syntactically. Module
@@ -1009,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)
@@ -1023,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.
@@ -1063,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)
@@ -1151,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))
@@ -1276,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)
@@ -1402,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 c7aa4b22..2daeb2e0 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.
@@ -1559,10 +1536,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'.
@@ -1597,7 +1574,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)
@@ -1734,12 +1711,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.
@@ -1828,7 +1805,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"	. ?¬)
     ;; ("/\\"	. ?∧)
@@ -1957,7 +1933,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
@@ -1982,26 +1958,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)
@@ -2060,7 +2035,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
@@ -2190,13 +2165,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
@@ -2326,7 +2301,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 ()
@@ -2455,7 +2430,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)
 
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
@@ -2479,7 +2454,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)
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;
@@ -2533,8 +2508,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))
 
@@ -2549,7 +2524,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."
@@ -3005,7 +2980,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)
 
 
 ;;
@@ -3102,9 +3077,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
@@ -3124,7 +3099,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
@@ -3174,9 +3149,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 "."
@@ -3306,7 +3283,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/generic/pg-pbrpm.el b/generic/pg-pbrpm.el
index f1f83ff1..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))
 
@@ -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/proof-menu.el b/generic/proof-menu.el
index ffd80415..dd3d05c8 100644
--- a/generic/proof-menu.el
+++ b/generic/proof-menu.el
@@ -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-utils.el b/generic/proof-utils.el
index 1568b2f0..4a15301a 100644
--- a/generic/proof-utils.el
+++ b/generic/proof-utils.el
@@ -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/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/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"