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.

1 files changed, 4 insertions, 3 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."