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.

3 files changed, 23 insertions, 24 deletions

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))))
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;;