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, 2 insertions, 6 deletions

diff --git a/coq/coq-system.el b/coq/coq-system.el
index bb1c28f0..bd0f7eba 100644
--- a/coq/coq-system.el
+++ b/coq/coq-system.el
@@ -1,4 +1,4 @@
-;;; coq-system.el --- common part of compilation feature
+;;; coq-system.el --- common part of compilation feature  -*- lexical-binding:t -*-
 
 ;; This file is part of Proof General.
 
@@ -25,10 +25,6 @@
 
 (require 'proof)
 
-(eval-when-compile
-  (require 'cl)
-  (require 'proof-compat))
-
 (defvar coq-prog-args)
 (defvar coq-debug)
 
@@ -514,7 +510,7 @@ coqtop."
         (`("-arg" ,concatenated-args)
          (setq args
                (append args
-                       (split-string-and-unquote (cadr opt) coq--project-file-separator))))))
+                       (split-string-and-unquote concatenated-args coq--project-file-separator))))))
     (cons "-emacs" args)))
 
 (defun coq--extract-load-path-1 (option base-directory)