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.

coq/coq-autotest.el

@@ -3,7 +3,7 @@
 ;; This file is part of Proof General.
 
 ;; Portions © Copyright 1994-2012  David Aspinall and University of Edinburgh
-;; Portions © Copyright 2003, 2012, 2014  Free Software Foundation, Inc.
+;; Portions © Copyright 2003-2018  Free Software Foundation, Inc.
 ;; Portions © Copyright 2001-2017  Pierre Courtieu
 ;; Portions © Copyright 2010, 2016  Erik Martin-Dorel
 ;; Portions © Copyright 2011-2013, 2016-2017  Hendrik Tews
@@ -16,9 +16,6 @@
 
 ;;; Code:
 
-(eval-when-compile
-  (require 'cl))
-
 (require 'pg-autotest)
 
 (require 'proof-site)

coq/coq-compile-common.el

@@ -22,6 +22,7 @@
 
 ;;; Code:
 
+(require 'cl-lib)                       ;cl-every cl-some
 (require 'proof-shell)
 (require 'coq-system)
 (require 'compile)
@@ -442,7 +443,7 @@ expressions in here are always matched against the .vo file name,
 regardless whether ``-quick'' would be used to compile the file
 or not."
   :type '(repeat regexp)
-  :safe (lambda (v) (every 'stringp v))
+  :safe (lambda (v) (cl-every #'stringp v))
   :group 'coq-auto-compile)
 
 (defcustom coq-coqdep-error-regexp
@@ -531,7 +532,7 @@ for instance, not make sense to let ProofGeneral check if the coq
 standard library is up-to-date.  This function is always invoked
 on the .vo file name, regardless whether the file would be
 compiled with ``-quick'' or not."
-  (if (some
+  (if (cl-some
        (lambda (dir-regexp) (string-match dir-regexp lib-obj-file))
        coq-compile-ignored-directories)
       (progn

coq/coq-db.el

@@ -1,9 +1,9 @@
-;;; coq-db.el --- coq keywords database utility functions -*- coding: utf-8; -*-
+;;; coq-db.el --- coq keywords database utility functions -*- coding: utf-8; lexical-binding:t -*-
 
 ;; This file is part of Proof General.
 
 ;; Portions © Copyright 1994-2012  David Aspinall and University of Edinburgh
-;; Portions © Copyright 2003, 2012, 2014  Free Software Foundation, Inc.
+;; Portions © Copyright 2003-2018  Free Software Foundation, Inc.
 ;; Portions © Copyright 2001-2017  Pierre Courtieu
 ;; Portions © Copyright 2010, 2016  Erik Martin-Dorel
 ;; Portions © Copyright 2011-2013, 2016-2017  Hendrik Tews
@@ -23,8 +23,7 @@
 
 ;;; Code:
 
-(eval-when-compile
-  (require 'cl))
+(eval-when-compile (require 'cl-lib))   ;decf
 
 (require 'proof-config)			; for proof-face-specs, a macro
 (require 'proof-syntax)			; for proof-ids-to-regexp
@@ -95,7 +94,7 @@ the first hole even if more than one."
 
 
 
-(defun coq-build-command-from-db (db prompt &optional preformatquery)
+(defun coq-build-command-from-db (db prompt &optional _preformatquery)
   "Ask for a keyword, with completion on keyword database DB and send to Coq.
 See `coq-syntax-db' for DB structure."
   ;; Next invocation of minibuffer (read-string below) will first recursively
@@ -192,8 +191,8 @@ Used by `coq-build-menu-from-db', which you should probably use instead.  See
 	     (menu     	 (nth 0 hd)) ; e1 = menu entry
 	     (abbrev   	 (nth 1 hd)) ; e2 = abbreviation
 	     (complt   	 (nth 2 hd)) ; e3 = completion
-	     (state    	 (nth 3 hd)) ; e4 = state changing
-	     (color    	 (nth 4 hd)) ; e5 = colorization string
+	     ;; (state   (nth 3 hd)) ; e4 = state changing
+	     ;; (color   (nth 4 hd)) ; e5 = colorization string
 	     (insertfn 	 (nth 5 hd)) ; e6 = function for smart insertion
 	     (menuhide 	 (nth 6 hd)) ; e7 = if non-nil : hide in menu
 	     (entry-with (max (- menuwidth (length menu)) 0))
@@ -212,7 +211,7 @@ Used by `coq-build-menu-from-db', which you should probably use instead.  See
 		  t)))
 	    (setq res (nconc res (list menu-entry)))));; append *in place*
 	(setq l (cdr l))
-	(decf size)))
+	(cl-decf size)))
     res))
 
 
@@ -264,9 +263,9 @@ See `coq-syntax-db' for DB structure."
   (let ((l db) (res ()))
     (while l
       (let* ((hd (car l))(tl (cdr l))	; hd is a list of length 3 or 4
-	     (e1 (car hd)) (tl1 (cdr hd)) ; e1 = menu entry
+	     (_e1 (car hd)) (tl1 (cdr hd)) ; e1 = menu entry
 	     (e2 (car tl1)) (tl2 (cdr tl1)) ; e2 = abbreviation
-	     (e3 (car tl2)) (tl3 (cdr tl2)) ; e3 = completion
+	     (e3 (car tl2)) (_tl3 (cdr tl2)) ; e3 = completion
 	     )
 	;; careful: nconc destructive!
 	(when e2

coq/coq-local-vars.el

@@ -1,4 +1,4 @@
-;;; coq-local-vars.el --- local variable list tools for coq
+;;; coq-local-vars.el --- local variable list tools for coq  -*- lexical-binding:t -*-
 
 ;; This file is part of Proof General.
 
@@ -19,9 +19,6 @@
 
 (require 'local-vars-list)              ; in lib directory
 
-(eval-when-compile
-  (require 'cl))
-
 (defvar coq-prog-name)
 (defvar coq-load-path)
 
@@ -136,7 +133,7 @@ Do not insert the default directory."
       ;; does not seem to exist in fsf emacs?? temporarily disable graphical
       ;; dialog, as read-file-name does not allow to select a directory
       ((current-use-dialog-box use-dialog-box)
-       (dummy (setq use-dialog-box nil))
+       (_dummy (setq use-dialog-box nil))
        (fname (file-name-nondirectory default))
        (dir (file-name-directory default))
        (path

coq/coq-par-compile.el

@@ -34,9 +34,6 @@
 
 ;;; Code:
 
-(eval-when-compile
-  (require 'proof-compat))
-
 (defvar queueitems)       ; dynamic scope in p-s-extend-queue-hook
 
 (require 'coq-compile-common)

coq/coq-seq-compile.el

@@ -24,9 +24,6 @@
 
 ;;; Code:
 
-(eval-when-compile
-  (require 'proof-compat))
-
 (defvar queueitems)       ; dynamic scope in p-s-extend-queue-hook
 
 (require 'coq-compile-common)

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)

coq/coq.el

@@ -19,10 +19,9 @@
 
 ;;; Code:
 
-(eval-when-compile
-  (require 'cl)
-  (require 'proof-compat))
+(require 'cl-lib)
 
+(require 'span)
 (eval-when-compile
   (require 'proof-utils)
   (require 'span)
@@ -37,10 +36,10 @@
 (defvar old-proof-marker)
 (defvar coq-keymap)
 (defvar coq-one-command-per-line)
-(defvar coq-auto-insert-as)    ; defpacustom
-(defvar coq-time-commands)        ; defpacustom
-(defvar coq-use-project-file)        ; defpacustom
-(defvar coq-use-editing-holes)    ; defpacustom
+(defvar coq-auto-insert-as)             ; defpacustom
+(defvar coq-time-commands)              ; defpacustom
+(defvar coq-use-project-file)           ; defpacustom
+(defvar coq-use-editing-holes)          ; defpacustom
 (defvar coq-hide-additional-subgoals)
 
 (require 'proof)
@@ -1585,7 +1584,7 @@ of hypothesis to highlight."
 See `coq-highlight-hyps-cited-in-response' and `SearchAbout'."
   (let* ((hyps-cited-pos (coq-detect-hyps-positions proof-response-buffer))
          (hyps-cited (coq-build-hyps-names hyps-cited-pos)))
-    (remove-if-not
+    (cl-remove-if-not
      (lambda (e)
        (cl-some;seq-find
         (lambda (f)
@@ -2536,7 +2535,7 @@ mouse activation."
 (defun coq-directories-files (l)
   (let* ((file-list-list (mapcar 'directory-files l))
          (file-list (apply 'append file-list-list))
-         (filtered-list (remove-if-not 'coq-postfix-.v-p file-list)))
+         (filtered-list (cl-remove-if-not #'coq-postfix-.v-p file-list)))
   filtered-list))
 
 (defun coq-remove-dot-v-extension (s)
@@ -2547,8 +2546,8 @@ mouse activation."
 
 (defun coq-build-accessible-modules-list ()
   (let* ((pth (or coq-load-path '(".")))
-         (cleanpth (mapcar 'coq-load-path-to-paths pth))
-         (existingpth (remove-if-not 'file-exists-p cleanpth))
+         (cleanpth (mapcar #'coq-load-path-to-paths pth))
+         (existingpth (cl-remove-if-not #'file-exists-p cleanpth))
          (file-list (coq-directories-files existingpth)))
     (mapcar 'coq-remove-dot-v-extension file-list)))
 
@@ -2586,11 +2585,11 @@ mouse activation."
           (completing-read
            "Command (TAB to see list, default Require Import) : "
            reqkinds-kinds-table nil nil nil nil "Require Import")))
-    (loop do
-          (setq s (completing-read "Name (empty to stop) : "
-                                   (coq-build-accessible-modules-list)))
-          (unless (zerop (length s)) (insert (format "%s %s.\n" reqkind s)))
-          while (not (string-equal s "")))))
+    (cl-loop do
+             (setq s (completing-read "Name (empty to stop) : "
+                                      (coq-build-accessible-modules-list)))
+             (unless (zerop (length s)) (insert (format "%s %s.\n" reqkind s)))
+             while (not (string-equal s "")))))
 
 ;; TODO add module closing
 (defun coq-end-Section ()
@@ -2731,16 +2730,16 @@ Also insert holes at insertion positions."
           (insert match)
           (indent-region start (point) nil)
           (let ((n (holes-replace-string-by-holes-backward start)))
-            (case n
-	(0 nil)				; no hole, stay here.
-	(1
-	 (goto-char start)
-	 (holes-set-point-next-hole-destroy)) ; if only one hole, go to it.
-	(t
-	 (goto-char start)
-	 (message
-          (substitute-command-keys
-           "\\[holes-set-point-next-hole-destroy] to jump to active hole.  \\[holes-short-doc] to see holes doc."))))))))))
+            (pcase n
+	      (0 nil)                   ; no hole, stay here.
+	      (1
+	       (goto-char start)
+	       (holes-set-point-next-hole-destroy)) ; if only one hole, go to it.
+	      (_
+	       (goto-char start)
+	       (message
+                (substitute-command-keys
+                 "\\[holes-set-point-next-hole-destroy] to jump to active hole.  \\[holes-short-doc] to see holes doc."))))))))))
 
 (defun coq-insert-solve-tactic ()
   "Ask for a closing tactic name, with completion, and insert at point.
@@ -3318,8 +3317,6 @@ priority to the former."
 
 (provide 'coq)
 
-
-
 ;;   Local Variables: ***
 ;;   fill-column: 79 ***
 ;;   indent-tabs-mode: nil ***

doc/docstring-magic.el

@@ -3,7 +3,7 @@
 ;; This file is part of Proof General.
 
 ;; Portions © Copyright 1994-2012  David Aspinall and University of Edinburgh
-;; Portions © Copyright 2003, 2012, 2014  Free Software Foundation, Inc.
+;; Portions © Copyright 2003-2018  Free Software Foundation, Inc.
 ;; Portions © Copyright 2001-2017  Pierre Courtieu
 ;; Portions © Copyright 2010, 2016  Erik Martin-Dorel
 ;; Portions © Copyright 2011-2013, 2016-2017  Hendrik Tews
@@ -23,7 +23,6 @@
       (append '("../generic/") load-path))
 (load "proof-site.el")
 (require 'proof-autoloads)
-(require 'proof-compat)
 (require 'proof-utils)
 
 

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"

generic/pg-assoc.el

@@ -3,7 +3,7 @@
 ;; This file is part of Proof General.
 
 ;; Portions © Copyright 1994-2012  David Aspinall and University of Edinburgh
-;; Portions © Copyright 2003, 2012, 2014  Free Software Foundation, Inc.
+;; Portions © Copyright 2003-2018  Free Software Foundation, Inc.
 ;; Portions © Copyright 2001-2017  Pierre Courtieu
 ;; Portions © Copyright 2010, 2016  Erik Martin-Dorel
 ;; Portions © Copyright 2011-2013, 2016-2017  Hendrik Tews
@@ -21,6 +21,7 @@
 
 ;;; Code:
 
+(require 'cl-lib)                       ;cl-remove-if-not
 (require 'proof-utils)
 
 (define-derived-mode proof-universal-keys-only-mode fundamental-mode
@@ -66,13 +67,13 @@ argument ALL-FRAMES has the same meaning than for
 
 (defun proof-filter-associated-windows (lw)
   "Remove windows of LW not displaying at least one associated buffer."
-  (remove-if-not (lambda (w) (proof-associated-buffer-p (window-buffer w))) lw))
+  (cl-remove-if-not (lambda (w) (proof-associated-buffer-p (window-buffer w))) lw))
 
 
 ;;;###autoload
 (defun proof-associated-frames ()
   "Return the list of frames displaying at least one associated buffer."
-  (remove-if-not (lambda (f) (proof-filter-associated-windows (window-list f)))
+  (cl-remove-if-not (lambda (f) (proof-filter-associated-windows (window-list f)))
 		 (frame-list)))
 
 (provide 'pg-assoc)

generic/pg-goals.el

@@ -19,7 +19,6 @@
 ;;; Code:
 (eval-when-compile
   (require 'easymenu)			; easy-menu-add, etc
-  (require 'cl)				; incf
   (require 'span))			; span-*
 (defvar proof-goals-mode-menu)          ; defined by macro below
 (defvar proof-assistant-menu)           ; defined by macro in proof-menu