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, 1 deletions

diff --git a/easycrypt/easycrypt.el b/easycrypt/easycrypt.el
index e9b40358..621805e7 100644
--- a/easycrypt/easycrypt.el
+++ b/easycrypt/easycrypt.el
@@ -10,6 +10,7 @@
 ;;; Commentary:
 ;; 
 
+(require 'cl-lib)                       ;cl-every
 (require 'proof)
 (require 'easycrypt-syntax)
 (require 'easycrypt-hooks)
@@ -24,7 +25,7 @@
 (defun easycrypt-load-path-safep (path)
   (and
    (listp path)
-   (every (lambda (entry) (stringp entry)) path)))
+   (cl-every #'stringp path)))
 
 ;; --------------------------------------------------------------------
 (defcustom easycrypt-prog-name "easycrypt"