Use `cl-lib` instead of `cl` everywhere

Use lexical-binding in a few files where it was easy.
Don't require `proof-compat` when it's not used.

* coq/coq-db.el: Use lexical-binding.

* coq/coq-system.el: Use lexical-binding.
(coq--extract-prog-args): Use concatenated-args rather than recomputing it.

* coq/coq.el: Require `span` to silence some warnings.

* generic/pg-user.el: Use lexical-binding.
(complete, add-completion, completion-min-length): Silence warnings.

* generic/pg-xml.el: Use lexical-binding.
(pg-xml-string-of): Prefer mapconcat to reduce+concat.

* generic/proof-depends.el: Use lexical-binding.
(proof-dep-split-deps): Use `push`.

* generic/proof-shell.el: Require `span` to silence some warnings.
(proof-shell-invisible-command): Don't use lexical-let just to build
a wasteful η-redex!

* lib/holes.el: Use lexical-binding.
Remove redundant :group args.

* lib/span.el: Use lexical-binding.
(span-read-only-hook): Use user-error.
(span-raise): Remove, unused.

1 files changed, 14 insertions, 16 deletions

diff --git a/generic/proof-shell.el b/generic/proof-shell.el
index 51d10c2c..a176283d 100644
--- a/generic/proof-shell.el
+++ b/generic/proof-shell.el
@@ -1,4 +1,4 @@
-;;; proof-shell.el --- Proof General shell mode.
+;;; proof-shell.el --- Proof General shell mode
 
 ;; This file is part of Proof General.
 
@@ -22,7 +22,7 @@
 
 ;;; Code:
 
-(require 'cl)				; set-difference, every
+(require 'cl-lib)                       ; cl-set-difference, cl-every
 
 (eval-when-compile
   (require 'span)
@@ -41,7 +41,7 @@
 (require 'pg-response)
 (require 'pg-goals)
 (require 'pg-user)			; proof-script, new-command-advance
-
+(require 'span)
 
 ;;
 ;; Internal variables used by proof shell
@@ -504,7 +504,7 @@ shell buffer, called by `proof-shell-bail-out' if process exits."
 	  (while (and (> timecount 0)
 		      (scomint-check-proc proof-shell-buffer))
 	    (accept-process-output proc 1 nil 1)
-	    (decf timecount)))
+	    (cl-decf timecount)))
 	
 	;; Still there, kill it rudely.
 	(when (memq (process-status proc) '(open run stop))
@@ -890,7 +890,7 @@ inserted text.
 Do not use this function directly, or output will be lost.  It is only
 used in `proof-add-to-queue' when we start processing a queue, and in
 `proof-shell-exec-loop', to process the next item."
-  (assert (or (stringp strings)
+  (cl-assert (or (stringp strings)
 	      (listp strings))
 	  nil "proof-shell-insert: expected string list argument")
 
@@ -1008,7 +1008,7 @@ being processed."
 	 (unless (eq proof-shell-busy queuemode)
 	   (proof-debug
 	    "proof-append-alist: wrong queuemode detected for busy shell")
-	   (assert (eq proof-shell-busy queuemode)))))
+	   (cl-assert (eq proof-shell-busy queuemode)))))
 
 
   (let ((nothingthere (null proof-action-list)))
@@ -1182,7 +1182,7 @@ contains only invisible elements for Prooftree synchronization."
 
 	(and (not proof-second-action-list-active)
 	     (or (null proof-action-list)
-		 (every
+		 (cl-every
 		  (lambda (item) (memq 'proof-tree-show-subgoal (nth 3 item)))
 		  proof-action-list)))))))
 
@@ -1310,8 +1310,8 @@ to `proof-register-possibly-new-processed-file'."
       ;; the proof-shell-compute-new-files-list
       (proof-restart-buffers
        (proof-files-to-buffers
-	(set-difference current-included
-			proof-included-files-list)))
+	(cl-set-difference current-included
+			   proof-included-files-list)))
       (cond
        ;; Do nothing if there was no active scripting buffer
        ((not scrbuf))
@@ -1762,7 +1762,7 @@ Only works when system timer has microsecond count available."
 	  (and
 	   (< (- tm pg-last-tracing-output-time)
 	      (/ pg-fast-tracing-mode-threshold 1000000.0))
-	   (>= (incf pg-last-trace-output-count)
+	   (>= (cl-incf pg-last-trace-output-count)
 	       pg-slow-mode-trigger-count))
 	;; quickly consecutive tracing outputs: go into slow mode
 	(setq dontprint t)
@@ -1856,16 +1856,14 @@ The flag 'invisible is always added to FLAGS."
 		    (not proof-shell-auto-terminate-commands)
 		    (string-match (concat
 				   (regexp-quote proof-terminal-string)
-				   "[ \t]*$") cmd))
+				   "[ \t]*$")
+                                  cmd))
 	  (setq cmd (concat cmd proof-terminal-string)))
 	(if wait (proof-shell-wait))
 	(proof-shell-ready-prover)  ; start proof assistant; set vars.
 	(let* ((callback
-		(if invisiblecallback
-		    (lexical-let ((icb invisiblecallback))
-		      (lambda (span)
-			(funcall icb span)))
-		  'proof-done-invisible)))
+		(or invisiblecallback
+		    #'proof-done-invisible)))
 	  (proof-start-queue nil nil
 			     (list (proof-shell-action-list-item
 				    cmd