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.

40 files changed, 252 insertions, 308 deletions

diff --git a/coq/coq-autotest.el b/coq/coq-autotest.el
index cecfdcf1..8be4bed9 100644
--- a/coq/coq-autotest.el
+++ b/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)
diff --git a/coq/coq-compile-common.el b/coq/coq-compile-common.el
index 9dca0082..d29bf1b9 100644
--- a/coq/coq-compile-common.el
+++ b/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
diff --git a/coq/coq-db.el b/coq/coq-db.el
index cad149a2..36812c4c 100644
--- a/coq/coq-db.el
+++ b/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
diff --git a/coq/coq-local-vars.el b/coq/coq-local-vars.el
index f172adbe..2211c22d 100644
--- a/coq/coq-local-vars.el
+++ b/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
diff --git a/coq/coq-par-compile.el b/coq/coq-par-compile.el
index b03fedaa..c6822dc5 100644
--- a/coq/coq-par-compile.el
+++ b/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)
diff --git a/coq/coq-seq-compile.el b/coq/coq-seq-compile.el
index 74327b53..4889ccaf 100644
--- a/coq/coq-seq-compile.el
+++ b/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)
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)
diff --git a/coq/coq.el b/coq/coq.el
index 6b1494a9..9fe52532 100644
--- a/coq/coq.el
+++ b/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 ***
diff --git a/doc/docstring-magic.el b/doc/docstring-magic.el
index 409fd22a..2943dd9f 100644
--- a/doc/docstring-magic.el
+++ b/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)
 
 
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"
diff --git a/generic/pg-assoc.el b/generic/pg-assoc.el
index b06b4ec5..59593ad6 100644
--- a/generic/pg-assoc.el
+++ b/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)
diff --git a/generic/pg-goals.el b/generic/pg-goals.el
index 124965e8..d9a350ec 100644
--- a/generic/pg-goals.el
+++ b/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
diff --git a/generic/pg-pgip.el b/generic/pg-pgip.el
index 0f427ecb..e84061b8 100644
--- a/generic/pg-pgip.el
+++ b/generic/pg-pgip.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
@@ -33,7 +33,7 @@
 ;;
 
 ;;; Code:
-(require 'cl)				; incf
+(require 'cl-lib)                       ; incf
 (require 'pg-xml)			;
 
 (declare-function pg-response-warning "pg-response")
@@ -55,8 +55,8 @@ The list PGIPS may contain one or more PGIP packets, whose contents are processe
   ;; PGIP processing is split into two steps:
   ;; (1) process each command, altering internal data structures
   ;; (2) post-process for each command type, affecting external interface (menus, etc).
-  (mapc 'pg-pgip-post-process
-	(reduce 'union (mapcar 'pg-pgip-process-pgip pgips))))
+  (mapc #'pg-pgip-post-process
+	(cl-reduce #'cl-union (mapcar #'pg-pgip-process-pgip pgips))))
 
 ;; TODO: use id's and sequence numbers to reconstruct streams of messages.
 (defvar pg-pgip-last-seen-id nil)
@@ -78,7 +78,7 @@ The list PGIPS may contain one or more PGIP packets, whose contents are processe
     (setq pg-pgip-last-seen-seq seq)
     (if (eq name 'pgip)
 	;; NB: schema currently allows only one message here
-	(mapcar 'pg-pgip-process-msg (xml-node-children pgip))
+	(mapcar #'pg-pgip-process-msg (xml-node-children pgip))
       (pg-internal-warning "pg-pgip-process-pgip: expected PGIP element, got %s" name))))
 
 (defun pg-pgip-process-msg (pgipmsg)
@@ -246,7 +246,7 @@ Return a symbol representing the PGIP command processed, or nil."
     (dolist (idtable idtables)
       (let* ((context  (pg-xml-get-attr 'context idtable 'optional))
 	     (objtype  (intern (pg-pgip-get-objtype idtable)))
-	     (idents   (mapcar 'pg-xml-get-text-content
+	     (idents   (mapcar #'pg-xml-get-text-content
 			       (xml-get-children idtable 'identifier)))
 	     (obarray  (or (and (not (eq opn 'setids))
 				(get objtype 'pgsymbols))
@@ -255,7 +255,7 @@ Return a symbol representing the PGIP command processed, or nil."
 	(setq proof-assistant-idtables
 	      (if (and (null idents) (eq opn 'setids))
 		  (delete objtype proof-assistant-idtables)
-		(adjoin objtype proof-assistant-idtables)))
+		(cl-adjoin objtype proof-assistant-idtables)))
 	(cond
 	 ((or (eq opn 'setids) (eq opn 'addids))
 	  (mapc (lambda (i) (intern i obarray)) idents))
@@ -400,7 +400,7 @@ Also sets local proverid and srcid variables for buffer."
       (with-current-buffer buffer
 	(make-local-variable 'proverid)
 	(setq proverid proverid))
-      (set pg-pgip-srcids (acons srcid (list buffer file) pg-pgip-srcids)))))
+      (set pg-pgip-srcids (cl-acons srcid (list buffer file) pg-pgip-srcids)))))
 
 
 ;; FIXME: right action?
@@ -483,7 +483,7 @@ Also sets local proverid and srcid variables for buffer."
 	  (list 'const val))))
      ((eq tyname 'pgipchoice)
       (let* ((choicesnodes  (pg-xml-child-elts node))
-	     (choices       (mapcar 'pg-pgip-get-pgiptype choicesnodes)))
+	     (choices       (mapcar #'pg-pgip-get-pgiptype choicesnodes)))
 	(list 'choice choices)))
      (t
       (pg-pgip-warning "pg-pgip-get-pgiptype: unrecognized/missing typename \"%s\"" tyname)))))
@@ -605,7 +605,7 @@ OTHERCLASS overrides this."
 					     "/" proof-assistant)))
 	 (id		(pg-xml-attr id pg-pgip-id))
 	 (class		(pg-xml-attr class (or otherclass "pa")))
-	 (seq		(pg-xml-attr seq (int-to-string (incf pg-pgip-seq))))
+	 (seq		(pg-xml-attr seq (int-to-string (cl-incf pg-pgip-seq))))
 	 (refseq        (if refseq (list (pg-xml-attr refseq refseq))))
 	 (refid         (if refid (list (pg-xml-attr refid refid))))
 	 (pgip_attrs	(append (list tag id class seq)
diff --git a/generic/pg-user.el b/generic/pg-user.el
index 5a5d6d13..a5ed27a9 100644
--- a/generic/pg-user.el
+++ b/generic/pg-user.el
@@ -1,4 +1,4 @@
-;;; pg-user.el --- User level commands for Proof General
+;;; pg-user.el --- User level commands for Proof General  -*- lexical-binding:t -*-
 
 ;; This file is part of Proof General.
 
@@ -26,9 +26,7 @@
 
 (require 'proof-script)	        ; we build on proof-script
 
-(require 'cl)
-(eval-when-compile
-  (require 'completion))                ; Loaded dynamically at runtime.
+(eval-when-compile (require 'cl-lib))   ;cl-decf
 (defvar which-func-modes)               ; Defined by which-func.
 
 (declare-function proof-segment-up-to "proof-script")
@@ -557,26 +555,29 @@ Uses `add-completion' with a negative number of uses and ancient
 last use time, to discourage saving these into the users database."
   (interactive)
   (require 'completion)
+  (defvar completion-min-length)
+  (declare-function add-completion "completion"
+                    (string &optional num-uses last-use-time))
   (mapcar (lambda (cmpl)
 	    ;; completion gives error; trapping is tricky so test again
 	    (if (>= (length cmpl) completion-min-length)
 		(add-completion cmpl -1000 0)))
 	  (proof-ass completion-table)))
 
-;; completion not autoloaded in GNU Emacs
-(or (fboundp 'complete)
-    (autoload 'complete "completion"))
-
 ;; NB: completion table is expected to be set when proof-script
 ;; is loaded!  Call `proof-script-add-completions' to update.
 
-(unless (bound-and-true-p byte-compile-current-file)
+(unless (bound-and-true-p byte-compile-current-file) ;FIXME: Yuck!
   (eval-after-load "completion"
     '(proof-add-completions)))
 
 (defun proof-script-complete (&optional arg)
-  "Like `complete' but case-fold-search set to proof-case-fold-search."
+  "Like `complete' but case-fold-search set to `proof-case-fold-search'."
   (interactive "*p")
+  ;; completion not autoloaded in GNU Emacs
+  ;; FIXME: It's probably because we shouldn't use it ;-)
+  (require 'completion)
+  (declare-function complete "completion" (&optional arg))
   (let ((case-fold-search proof-case-fold-search))
     (complete arg)))
 
@@ -889,13 +890,12 @@ a popup with the information in it."
 	(pg-identifier-query
 	 identifier ctxt
 	 ;; the callback
-	 (lexical-let ((s start) (e end))
-	   (lambda (x)
-	     (save-excursion
-	       (let ((idspan (span-make s e)))
-                 ;; (span-set-property idspan 'priority 90) ; highest
-                 (span-set-property idspan 'help-echo
-                                    (pg-last-output-displayform))))))))))
+	 (lambda (_)
+	   (save-excursion
+	     (let ((idspan (span-make start end)))
+               ;; (span-set-property idspan 'priority 90) ; highest
+               (span-set-property idspan 'help-echo
+                                  (pg-last-output-displayform)))))))))
 
 (defvar proof-query-identifier-history nil
   "History for `proof-query-identifier'.")
@@ -1253,7 +1253,7 @@ the locked region."
       (while (> repeat 0)
 	(pg-protected-undo-1 newarg) ; do some safe undos step by step
 	(setq last-command 'undo) ; need for this assignment meanwhile
-	(decf repeat)))))
+	(cl-decf repeat)))))
 
 (defun pg-protected-undo-1 (arg)
   "This function is intended to be called by `pg-protected-undo'.
diff --git a/generic/pg-xml.el b/generic/pg-xml.el
index 18285572..4e5ea385 100644
--- a/generic/pg-xml.el
+++ b/generic/pg-xml.el
@@ -1,9 +1,9 @@
-;;; pg-xml.el --- XML functions for Proof General
+;;; pg-xml.el --- XML functions for Proof General  -*- 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
@@ -20,8 +20,7 @@
 
 ;;; Code:
 
-(require 'cl)
-
+(require 'cl-lib)                       ;cl-mapcan
 (require 'xml)
 
 (require 'proof-utils) ;; for pg-internal-warning
@@ -90,7 +89,7 @@ Optional START and END bound the parse."
 (defun pg-xml-child-elts (node)
   "Return list of *element* children of NODE (ignoring strings)."
   (let ((children (xml-node-children node)))
-    (mapcan (lambda (x) (if (listp x) (list x))) children)))
+    (cl-mapcan (lambda (x) (if (listp x) (list x))) children)))
 
 (defun pg-xml-child-elt (node)
   "Return unique element child of NODE."
@@ -134,10 +133,10 @@ Optional START and END bound the parse."
   "Convert the XML trees in XMLS into a string (without additional indentation)."
   (let* (strs
 	 (insertfn    (lambda (&rest args)
-			(setq strs (cons (reduce 'concat args) strs)))))
+			(push (mapconcat #'identity args "") strs))))
     (dolist (xml xmls)
       (pg-xml-output-internal xml nil insertfn))
-    (reduce 'concat (reverse strs))))
+    (mapconcat #'identity (reverse strs) "")))
 
 ;; based on xml-debug-print from xml.el
 
@@ -187,7 +186,7 @@ Cal OUTPUTFN, which should accept a list of args."
 (defsubst pg-pgip-get-area (node &optional optional defaultval)
   (pg-xml-get-attr 'area node optional defaultval))
 
-(defun pg-pgip-get-icon (node &optional optional defaultval)
+(defun pg-pgip-get-icon (node &optional _optional _defaultval)
   "Return the <icon> child of NODE, or nil if none."
   (pg-xml-get-child 'icon node))
 
diff --git a/generic/proof-depends.el b/generic/proof-depends.el
index 72beb1d2..9f3b469a 100644
--- a/generic/proof-depends.el
+++ b/generic/proof-depends.el
@@ -1,9 +1,9 @@
-;;; proof-depends.el --- Theorem-theorem and theorem-definition dependencies
+;;; proof-depends.el --- Theorem-theorem and theorem-definition dependencies  -*- 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,7 +23,7 @@
 ;;
 
 ;;; Code:
-(require 'cl)
+(require 'cl-lib)
 (require 'span)
 (require 'pg-vars)
 (require 'proof-config)
@@ -191,12 +191,11 @@ Called from `proof-done-advancing' when a save is processed and
 	     (subitems (and ns (assoc ns nested))))
 	(cond
 	 ((and ns subitems)
-	  (setcdr subitems (adjoin name (cdr subitems))))
+	  (setcdr subitems (cl-adjoin name (cdr subitems))))
 	 (ns
-	  (setq nested
-		(cons (cons ns (list name)) nested)))
+	  (push (cons ns (list name)) nested))
 	 (t
-	  (setq toplevel (adjoin name  toplevel))))))
+	  (setq toplevel (cl-adjoin name  toplevel))))))
     (cons nested toplevel)))
 
 (defun proof-dep-make-submenu (name namefn appfn list)
@@ -221,7 +220,7 @@ NAMEFN is applied to each element of LIST to make the names."
 ;; Functions triggered by menus
 ;;
 
-(defun proof-goto-dependency (name span)
+(defun proof-goto-dependency (_name span)
   "Go to the start of SPAN."
   ;; FIXME(EMD): seems buggy as NAME is not used
   ;; FIXME: check buffer is right one.  Later we'll allow switching buffer
diff --git a/generic/proof-maths-menu.el b/generic/proof-maths-menu.el
index b1155557..6ff81c90 100644
--- a/generic/proof-maths-menu.el
+++ b/generic/proof-maths-menu.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
@@ -27,9 +27,6 @@
 ;;; Code:
 
 (eval-when-compile
-  (require 'cl))
-
-(eval-when-compile
   (require 'proof-auxmodes)	  ; loaded by proof.el
   (require 'maths-menu))	  ; loaded dynamically in proof-auxmodes
 
diff --git a/generic/proof-menu.el b/generic/proof-menu.el
index 027d0c7d..e43efcc0 100644
--- a/generic/proof-menu.el
+++ b/generic/proof-menu.el
@@ -17,7 +17,7 @@
 ;;
 
 ;;; Code:
-(require 'cl)				; mapcan
+(require 'cl-lib)                       ; cl-mapcan, ...
 
 (defvar proof-assistant-menu)  ; defined by macro in proof-menu-define-specific
 (defvar proof-mode-map)
@@ -49,24 +49,26 @@ without adjusting window layout."
   (cond
    ((and (called-interactively-p 'any)
 	 (eq last-command 'proof-display-some-buffers))
-    (incf proof-display-some-buffers-count))
+    (cl-incf proof-display-some-buffers-count))
    (t
     (setq proof-display-some-buffers-count 0)))
-  (let* ((assocbufs   (remove-if-not 'buffer-live-p
-				     (list proof-response-buffer
-					   proof-thms-buffer
-					   proof-trace-buffer
-					   proof-goals-buffer
-					   )))
+  (let* ((assocbufs   (cl-remove-if-not #'buffer-live-p
+				        (list proof-response-buffer
+					      proof-thms-buffer
+					      proof-trace-buffer
+					      proof-goals-buffer
+					      )))
 					;proof-shell-buffer
 	 (numassoc    (length assocbufs)))
     ;; If there's no live other buffers, we don't do anything.
     (unless (zerop numassoc)
       (let
 	 ((selectedbuf (nth (mod proof-display-some-buffers-count
-				 numassoc) assocbufs))
+				 numassoc)
+                            assocbufs))
 	  (nextbuf     (nth (mod (1+ proof-display-some-buffers-count)
-				 numassoc) assocbufs)))
+				 numassoc)
+                            assocbufs)))
 	(cond
 	 ((or proof-three-window-enable proof-multiple-frames-enable)
 	  ;; Display two buffers: next in rotation and goals/response
@@ -74,7 +76,8 @@ without adjusting window layout."
 	  (proof-switch-to-buffer selectedbuf 'noselect)
 	  (proof-switch-to-buffer (if (eq selectedbuf proof-goals-buffer)
 				      proof-response-buffer
-				    proof-goals-buffer) 'noselect))
+				    proof-goals-buffer)
+                                  'noselect))
 	 (selectedbuf
 	  (proof-switch-to-buffer selectedbuf 'noselect)))
 	(if (eq selectedbuf proof-response-buffer)
@@ -755,7 +758,7 @@ suitable for adding to the proof assistant menu."
     (while (and new (fboundp menu-fn))
       (setq menu-fn (intern (concat (symbol-name menuname-sym)
 				    "-" (int-to-string i))))
-      (incf i))
+      (cl-incf i))
     (if inscript
 	(eval `(proof-defshortcut ,menu-fn ,command ,key))
       (eval `(proof-definvisible ,menu-fn ,command ,key)))
@@ -789,7 +792,7 @@ suitable for adding to the proof assistant menu."
 		     nil t)))
   (let*
       ((favs       (proof-ass favourites))
-       (rmfavs	   (remove-if
+       (rmfavs	   (cl-remove-if
 		    (lambda (f) (string-equal menuname (caddr f)))
 		    favs)))
     (unless (equal favs rmfavs)
@@ -831,7 +834,7 @@ KEY is the optional key binding."
   (let*
       ((menu-entry (proof-def-favourite command inscript menuname key t))
        (favs       (proof-ass favourites))
-       (rmfavs	   (remove-if
+       (rmfavs	   (cl-remove-if
 		    (lambda (f) (string-equal menuname (caddr f)))
 		    favs))
        (newfavs    (append
@@ -860,7 +863,7 @@ KEY is the optional key binding."
 	(mapc (lambda (stg) (add-to-list 'groups (get (car stg) 'pggroup)))
 	      proof-assistant-settings)
 	(dolist (grp (reverse groups))
-	  (let* ((gstgs (mapcan (lambda (stg)
+	  (let* ((gstgs (cl-mapcan (lambda (stg)
 				  (if (eq (get (car stg) 'pggroup) grp)
 				      (list stg)))
 				proof-assistant-settings))
diff --git a/generic/proof-script.el b/generic/proof-script.el
index 9c5c06a4..4c56fc7b 100644
--- a/generic/proof-script.el
+++ b/generic/proof-script.el
@@ -24,7 +24,7 @@
 
 ;;; Code:
 
-(require 'cl)				; various
+(require 'cl-lib)                       ; various
 (require 'span)				; abstraction of overlays/extents
 (require 'proof-utils)			; proof-utils macros
 (require 'proof-syntax)			; utils for manipulating syntax
@@ -520,8 +520,8 @@ Intended as a hook function for `proof-shell-handle-error-or-interrupt-hook'."
 (defun pg-get-element (idiomsym id)
   "Return proof script element of type IDIOMSYM with identifier ID.
 IDIOMSYM is a symbol, ID is a string."
-  (assert (symbolp idiomsym))
-  (assert (stringp id))
+  (cl-assert (symbolp idiomsym))
+  (cl-assert (stringp id))
   (let ((idsym  (intern id))
 	(elts   (cdr-safe (assq idiomsym pg-script-portions))))
     (if elts
@@ -539,9 +539,9 @@ NAME does not need to be unique.
 
 NAME is a name that comes from the proof script or prover output.
 It is recorded in the span with the 'rawname property."
-  (assert (symbolp idiomsym))
-  (assert (stringp id))
-  (if name (assert (stringp name)))
+  (cl-assert (symbolp idiomsym))
+  (cl-assert (stringp id))
+  (if name (cl-assert (stringp name)))
   (let* ((idsym    (intern id))
 	 (rawname  name)
 	 (name	   (or name id))
@@ -880,8 +880,8 @@ proof assistant and Emacs has a modified buffer visiting the file."
       (funcall proof-shell-inform-file-retracted-cmd rfile)
       (proof-restart-buffers
        (proof-files-to-buffers
-	(set-difference current-included
-			proof-included-files-list)))))))
+	(cl-set-difference current-included
+			   proof-included-files-list)))))))
 
 (defun proof-auto-retract-dependencies (cfile &optional informprover)
   "Perhaps automatically retract the (linear) dependencies of CFILE.
@@ -1234,8 +1234,8 @@ activation is considered to have failed and an error is given."
       ;; proof-unregister-buffer-file-name.
       (if proof-script-buffer
 	  (proof-deactivate-scripting))
-      (assert (null proof-script-buffer)
-	      "Bug in proof-activate-scripting: deactivate failed.")
+      (cl-assert (null proof-script-buffer)
+	         "Bug in proof-activate-scripting: deactivate failed.")
 
       ;; Set the active scripting buffer
       (setq proof-script-buffer (current-buffer))
@@ -1340,7 +1340,7 @@ Argument SPAN has just been processed."
      ;; CASE 2: Save command seen, now we may amalgamate spans.
      ((and (proof-string-match-safe proof-save-command-regexp cmd)
 	   (funcall proof-really-save-command-p span cmd)
-	   (decf proof-nesting-depth) ;; [always non-nil/true]
+	   (cl-decf proof-nesting-depth) ;; [always non-nil/true]
 	   (if proof-nested-goals-history-p
 	       ;; For now, we only support this nesting behaviour:
 	       ;; don't amalgamate unless the nesting depth is 0,
@@ -1479,15 +1479,15 @@ Argument SPAN has just been processed."
 	     ((and proof-nested-goals-history-p
 		   proof-save-command-regexp
 		   (proof-string-match proof-save-command-regexp cmd))
-	      (incf lev))
+	      (cl-incf lev))
 	     ;; Decrement depth when a goal is hit
 	     ((funcall proof-goal-command-p gspan)
-	      (decf lev))
+	      (cl-decf lev))
 	     ;; Remainder cases: see if command matches something we
 	     ;; should count for a global undo
 	     ((and proof-nested-undo-regexp
 		   (proof-string-match proof-nested-undo-regexp cmd))
-	      (incf nestedundos))
+	      (cl-incf nestedundos))
 	     ))))
 
     (if (not gspan)
@@ -1556,7 +1556,7 @@ Subroutine of `proof-done-advancing-save'."
   ;; In the extend case, the context of proof grows until hit a save
   ;; or new goal.
   (if (eq proof-completed-proof-behaviour 'extend)
-      (incf proof-shell-proof-completed)
+      (cl-incf proof-shell-proof-completed)
     (setq proof-shell-proof-completed nil))
 
   (let* ((swallow  (eq proof-completed-proof-behaviour 'extend))
@@ -1623,12 +1623,12 @@ Subroutine of `proof-done-advancing-save'."
   (cond
    ((funcall proof-goal-command-p span)
     (pg-add-element 'statement id bodyspan)
-    (incf proof-nesting-depth))
+    (cl-incf proof-nesting-depth))
    (t
     (pg-add-element 'command id bodyspan)))
 
   (if proof-shell-proof-completed
-      (incf proof-shell-proof-completed))
+      (cl-incf proof-shell-proof-completed))
 
   (pg-set-span-helphighlights span proof-command-mouse-highlight-face)))
 
@@ -1969,7 +1969,7 @@ We assume that the list is contiguous and begins at (proof-queue-or-locked-end).
 We also delete help spans which appear in the same region (in the expectation
 that these may be overwritten).
 This function expects the buffer to be activated for advancing."
-  (assert semis nil "proof-assert-semis: argument must be a list")
+  (cl-assert semis nil "proof-assert-semis: argument must be a list")
   (let ((startpos  (proof-queue-or-locked-end))
 	(lastpos   (nth 2 (car semis)))
 	(vanillas  (proof-semis-to-vanillas semis displayflags)))
@@ -2458,13 +2458,13 @@ For this function to work properly, you must configure
       (setq str (span-property span 'cmd))
       (cond ((eq (span-property span 'type) 'vanilla)
 	     (unless (proof-stringfn-match proof-ignore-for-undo-count str)
-	       (incf ct)))
+	       (cl-incf ct)))
 	    ((eq (span-property span 'type) 'pbp)
 	     (setq i 0)
 	     (while (< i (length str))
 	       (if (string-equal (substring str i (+ i tl)) proof-terminal-string)
-		   (incf ct))
-	       (incf i))))
+		   (cl-incf ct))
+	       (cl-incf i))))
       (setq span (next-span span 'type)))
     (if (= ct 0)
 	nil ; was proof-no-command
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
diff --git a/generic/proof-syntax.el b/generic/proof-syntax.el
index 5871a993..e93f5ca4 100644
--- a/generic/proof-syntax.el
+++ b/generic/proof-syntax.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
@@ -20,7 +20,6 @@
 ;;; Code:
 (require 'font-lock)
 (require 'proof-config)			; proof-case-fold-search
-(require 'proof-compat)			; proof-buffer-syntactic-context
 (require 'pg-pamacs)			; proof-ass-sym
 
 (defsubst proof-ids-to-regexp (l)
diff --git a/generic/proof-tree.el b/generic/proof-tree.el
index cb85952d..c7afe212 100644
--- a/generic/proof-tree.el
+++ b/generic/proof-tree.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
@@ -93,8 +93,7 @@
 
 ;;; Code:
 
-(require 'cl)
-
+(eval-when-compile (require 'cl-lib))   ;cl-assert
 (eval-when-compile
   (require 'proof-shell))
 
@@ -622,7 +621,7 @@ primitives is changed.")
 Send a message with command line SECOND-LINE and all strings in
 DATA as data sections to Prooftree."
   (let ((second-line-len (string-bytes second-line)))
-    (assert (< second-line-len 999))
+    (cl-assert (< second-line-len 999))
     (process-send-string
      proof-tree-process
      (format "second line %03d\n%s\n%s%s"
@@ -1157,7 +1156,7 @@ entry that is now finally retired.  CMD is the command, FLAGS are
 the flags and SPAN is the span."
   ;; (message "PTHDO cmd %s flags %s span %s-%s" cmd flags
   ;; 	   (if span (span-start span)) (if span (span-end span)))
-  (assert proof-tree-external-display)
+  (cl-assert proof-tree-external-display)
   (unless (or (memq 'invisible flags) (memq 'proof-tree-show-subgoal flags))
     (let* ((proof-info (funcall proof-tree-get-proof-info))
 	   (current-proof-name (cadr proof-info)))
@@ -1226,7 +1225,7 @@ position of the current proof."
     (error
      "Enabling prooftree inside a proof outside the current scripting buffer"))
   (proof-shell-ready-prover)
-  (assert proof-locked-span)
+  (cl-assert proof-locked-span)
   (message "Start proof-tree display for current proof")
   (save-excursion
     (save-window-excursion
diff --git a/generic/proof-unicode-tokens.el b/generic/proof-unicode-tokens.el
index 2deca0e6..7ae75ba1 100644
--- a/generic/proof-unicode-tokens.el
+++ b/generic/proof-unicode-tokens.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
@@ -25,9 +25,6 @@
 ;;; Code:
 
 (eval-when-compile
-  (require 'cl))
-
-(eval-when-compile
   (require 'scomint)
   (require 'proof-auxmodes)	 ; loaded by proof.el, autoloads us
   (require 'unicode-tokens))	 ; it will be loaded by proof-auxmodes
diff --git a/generic/proof-utils.el b/generic/proof-utils.el
index a2c29824..99e537c5 100644
--- a/generic/proof-utils.el
+++ b/generic/proof-utils.el
@@ -51,7 +51,6 @@
 
 
 (require 'proof-site)			; basic vars
-(require 'proof-compat)		        ; compatibility
 (require 'pg-pamacs)			; macros for pa config
 (require 'proof-config)			; config vars
 (require 'bufhist)			; bufhist
diff --git a/generic/proof.el b/generic/proof.el
index 5fa9de33..f3b3b276 100644
--- a/generic/proof.el
+++ b/generic/proof.el
@@ -1,9 +1,9 @@
-;;; proof.el --- Proof General theorem prover interface.
+;;; proof.el --- Proof General theorem prover interface
 
 ;; 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
@@ -36,7 +36,6 @@
 (unless (or noninteractive (bound-and-true-p byte-compile-current-file))
   (proof-splash-message))		; welcome the user now.
 
-(require 'proof-compat)			; Emacs and OS compatibility
 (require 'proof-utils)			; utilities
 (require 'proof-config)			; configuration variables
 (require 'proof-auxmodes)		; auxmode functions
diff --git a/hol-light/hol-light-autotest.el b/hol-light/hol-light-autotest.el
index d68b898f..dab2c4c4 100644
--- a/hol-light/hol-light-autotest.el
+++ b/hol-light/hol-light-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, 2012, 2014, 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 'proof-site)
 (proof-ready-for-assistant 'hol-light)
 
diff --git a/isar/isabelle-system.el b/isar/isabelle-system.el
index 0b61aab0..4fb2bcde 100644
--- a/isar/isabelle-system.el
+++ b/isar/isabelle-system.el
@@ -13,9 +13,8 @@
 ;;
 
 ;;; Code:
-(eval-when-compile
-  (require 'cl))			;  mapcan, eval-when
 
+(require 'cl-lib)                       ;cl-mapcan
 (eval-when-compile
   (require 'span)
   (require 'scomint)
@@ -234,7 +233,7 @@ passed to isa-tool-doc-command, DOCNAME will be viewed."
       (let ((docs (isa-shell-command-to-string
 		   (concat "\"" isa-isabelle-command "\" doc"))))
 	(unless (string-equal docs "")
-	  (mapcan
+	  (cl-mapcan
 	   (function (lambda (docdes)
 		       (if (proof-string-match "^[ \t]+\\(\\S-+\\)[ \t]+" docdes)
 			   (list (list
diff --git a/isar/isar-autotest.el b/isar/isar-autotest.el
index f8784bc2..8e098a29 100644
--- a/isar/isar-autotest.el
+++ b/isar/isar-autotest.el
@@ -10,9 +10,6 @@
 
 (require 'pg-autotest)
 
-(eval-when-compile
-  (require 'cl))
-
 (require 'proof-site)
 (proof-ready-for-assistant 'isar)
 
diff --git a/isar/isar-profiling.el b/isar/isar-profiling.el
index 0cf19348..ae8a8f8c 100644
--- a/isar/isar-profiling.el
+++ b/isar/isar-profiling.el
@@ -5,9 +5,6 @@
 ;; $Id$
 ;;
 
-(eval-when-compile
-  (require 'cl))
-
 (require 'proof-site)
 (proof-ready-for-assistant 'isar)
 
diff --git a/isar/isar-syntax.el b/isar/isar-syntax.el
index 7fa6f55d..095b108c 100644
--- a/isar/isar-syntax.el
+++ b/isar/isar-syntax.el
@@ -8,7 +8,7 @@
 ;; $Id$
 ;;
 
-(require 'cl)				; remove-if, remove-if-not
+(eval-when-compile (require 'cl-lib))
 
 (require 'proof-syntax)
 (require 'isar-keywords)		; NB: we want to load isar-keywords at runtime
@@ -271,18 +271,18 @@ matches contents of quotes for quoted identifiers.")
       (while (proof-re-search-forward isar-nesting-regexp limit t)
 	(cond
 	 ((proof-buffer-syntactic-context))
-	 ((equal (match-string 0) isar-keyword-begin) (incf nesting))
-	 ((equal (match-string 0) isar-keyword-end) (decf nesting)))))
+	 ((equal (match-string 0) isar-keyword-begin) (cl-incf nesting))
+	 ((equal (match-string 0) isar-keyword-end) (cl-decf nesting)))))
     nesting))
 
 (defun isar-match-nesting (limit)
-  (block nil
+  (cl-block nil
     (while (proof-re-search-forward isar-nesting-regexp limit t)
       (and (not (proof-buffer-syntactic-context))
 	   (if (equal (match-string 0) isar-keyword-begin)
 	       (> (isar-nesting) 1)
 	     (> (isar-nesting) 0))
-	   (return t)))))
+	   (cl-return t)))))
 
 
 ;; ----- Isabelle inner syntax highlight
diff --git a/isar/isar-unicode-tokens.el b/isar/isar-unicode-tokens.el
index c6f58452..725bc544 100644
--- a/isar/isar-unicode-tokens.el
+++ b/isar/isar-unicode-tokens.el
@@ -12,7 +12,7 @@
 ;;
 
 
-(require 'cl)				; for-loop
+(eval-when-compile (require 'cl-lib))   ; cl-loop
 
 (eval-when-compile
   (require 'unicode-tokens)	    ; it's loaded dynamically at runtime
@@ -481,10 +481,10 @@ tokens."
   :set 'isar-set-and-restart-tokens)
 
 (defun isar-map-letters (f1 f2 &rest symbs)
-  (loop for x below 26
-	for c = (+ 65 x)
-	collect
-	(cons (funcall f1 c) (cons (funcall f2 c) symbs))))
+  (cl-loop for x below 26
+	   for c = (+ 65 x)
+	   collect
+	   (cons (funcall f1 c) (cons (funcall f2 c) symbs))))
 
 (defconst isar-script-letters-tokens ; \<A> \<B> ...
   (isar-map-letters (lambda (x) (format "%c" x))
diff --git a/isar/isar.el b/isar/isar.el
index 917f8f6a..9deed7c1 100644
--- a/isar/isar.el
+++ b/isar/isar.el
@@ -17,9 +17,6 @@
 
 ;;; Code:
 
-(eval-when-compile 
-  (require 'cl))
-
 (eval-when-compile
   (require 'span)
   (require 'proof-syntax)
diff --git a/lego/lego.el b/lego/lego.el
index 29564c87..248e9d09 100644
--- a/lego/lego.el
+++ b/lego/lego.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
@@ -19,6 +19,7 @@
 
 ;;; Code:
 
+(require 'cl-lib)                       ;cl-member-if
 (require 'proof)
 (require 'lego-syntax)
 (eval-when-compile
@@ -376,7 +377,7 @@ Value for `proof-shell-compute-new-files-list', which see.
 
 For LEGO, we assume that module identifiers coincide with file names."
   (let ((module (match-string 1)))
-    (cdr (member-if
+    (cdr (cl-member-if
 	  (lambda (filename) (lego-equal-module-filename module filename))
 	  proof-included-files-list))))
 
diff --git a/lib/holes.el b/lib/holes.el
index 9a45037c..84dcf1f3 100644
--- a/lib/holes.el
+++ b/lib/holes.el
@@ -1,9 +1,9 @@
-;;; holes.el --- a little piece of elisp to define holes in your buffer
+;;; holes.el --- a little piece of elisp to define holes in your buffer  -*- 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
@@ -36,7 +36,7 @@
 
 ;;; Code:
 (require 'span)
-(require 'cl)
+(eval-when-compile (require 'cl-lib))
 
 ;;;
 ;;; initialization
@@ -65,16 +65,14 @@ and this is this one.  This is not buffer local.")
 
 (defcustom holes-empty-hole-string "#"
   "String to be inserted for empty hole (don't put an empty string)."
-  :type 'string
-  :group 'holes)
+  :type 'string)
 
 (defcustom holes-empty-hole-regexp "#\\|@{\\([^{}]*\\)}"
   "Regexp denoting a hole in abbrevs.
 Subgroup 1 is treated specially: if it matches, it is assumed that
 everything before it and after it in the regexp matches delimiters
 which should be removed when making the text into a hole."
-  :type 'regexp
-  :group 'holes)
+  :type 'regexp)
 
 
 ;(defcustom holes-search-limit 1000
@@ -97,8 +95,7 @@ which should be removed when making the text into a hole."
      :background "darkred" :foreground "white")
     (((class color) (background light))
      :background "paleVioletRed" :foreground "black"))
-  "Font Lock face used to highlight the active hole."
-  :group 'holes)
+  "Font Lock face used to highlight the active hole.")
 
 (defface inactive-hole-face
   '((((class grayscale) (background light)) :background "lightgrey")
@@ -107,8 +104,7 @@ which should be removed when making the text into a hole."
      :background "mediumblue" :foreground "white")
     (((class color) (background light))
      :background "lightsteelblue" :foreground "black"))
-  "Font Lock  face used to highlight the active hole."
-  :group 'holes)
+  "Font Lock  face used to highlight the active hole.")
 
 ;;;
 ;;; Keymaps
@@ -180,7 +176,7 @@ This is not the keymap used on holes's overlay (see `hole-map' instead).")
 
 (defun holes-copy-active-region ()
   "Copy and retuurn the active region."
-  (assert mark-active nil "the region is not active now.")
+  (cl-assert mark-active nil "the region is not active now.")
   (copy-region-as-kill (region-beginning) (region-end))
   (car kill-ring))
 
@@ -190,19 +186,19 @@ This is not the keymap used on holes's overlay (see `hole-map' instead).")
 
 (defun holes-hole-start-position (hole)
   "Return start position of HOLE."
-  (assert (holes-is-hole-p hole) t
+  (cl-assert (holes-is-hole-p hole) t
 	  "holes-hole-start-position: %s is not a hole")
   (span-start hole))
 
 (defun holes-hole-end-position (hole)
   "Return end position of HOLE."
-  (assert (holes-is-hole-p hole) t "holes-hole-end-position: %s is not a hole")
+  (cl-assert (holes-is-hole-p hole) t "holes-hole-end-position: %s is not a hole")
   (span-end hole))
 
 (defun holes-hole-buffer (hole)
   "Return the buffer of HOLE."
   "Internal."
-  (assert (holes-is-hole-p hole) t "holes-hole-buffer: %s is not a hole")
+  (cl-assert (holes-is-hole-p hole) t "holes-hole-buffer: %s is not a hole")
   (span-buffer hole))
 
 (defun holes-hole-at (&optional pos)
@@ -221,7 +217,7 @@ active-hole-marker variable)."
   "Return the position of the start of the active hole.
 See `active-hole-buffer' to get its buffer.  Returns an error if
 active hole doesn't exist (the marker is set to nothing)."
-  (assert (holes-active-hole-exist-p) t
+  (cl-assert (holes-active-hole-exist-p) t
 	  "holes-active-hole-start-position: no active hole")
   (holes-hole-start-position holes-active-hole))
 
@@ -229,7 +225,7 @@ active hole doesn't exist (the marker is set to nothing)."
   "Return the position of the start of the active hole.
 See `active-hole-buffer' to get its buffer.  Returns an error if
 active hole doesn't exist (the marker is set to nothing)."
-  (assert (holes-active-hole-exist-p) t
+  (cl-assert (holes-active-hole-exist-p) t
 	  "holes-active-hole-end-position: no active hole")
   (holes-hole-end-position holes-active-hole))
 
@@ -238,7 +234,7 @@ active hole doesn't exist (the marker is set to nothing)."
   "Return the buffer containing the active hole.
 Raise an error if the active hole is not set.  Don't care if the
 active hole is empty."
-  (assert (holes-active-hole-exist-p) t
+  (cl-assert (holes-active-hole-exist-p) t
 	  "holes-active-hole-buffer: no active hole")
   (holes-hole-buffer holes-active-hole))
 
@@ -246,7 +242,7 @@ active hole is empty."
   "Set point to active hole.
 Raises an error if active-hole is not set."
   (interactive)
-  (assert (holes-active-hole-exist-p) t
+  (cl-assert (holes-active-hole-exist-p) t
 	  "holes-goto-active-hole: no active hole")
   (goto-char (holes-active-hole-start-position)))
 
@@ -255,7 +251,7 @@ Raises an error if active-hole is not set."
   "Highlight a HOLE with the `active-hole-face'.
 DON'T USE this as it would break synchronization (non active hole
 highlighted)."
-  (assert (holes-is-hole-p hole) t
+  (cl-assert (holes-is-hole-p hole) t
 	  "holes-highlight-hole-as-active: %s is not a hole")
   (set-span-face hole 'active-hole-face))
 
@@ -263,7 +259,7 @@ highlighted)."
   "Highlight a HOLE with the not active face.
 DON'T USE this as it would break synchronization (active hole non
 highlighted)."
-  (assert (holes-is-hole-p hole) t
+  (cl-assert (holes-is-hole-p hole) t
 	  "holes-highlight-hole: %s is not a hole")
   (set-span-face hole 'inactive-hole-face))
 
@@ -283,7 +279,7 @@ the active hole is already disable."
 (defun holes-set-active-hole (hole)
   "Set active hole to HOLE.
 Error if HOLE is not a hole."
-  (assert (holes-is-hole-p hole) t
+  (cl-assert (holes-is-hole-p hole) t
 	  "holes-set-active-hole: %s is not a hole")
   (if (holes-active-hole-exist-p)
       (holes-highlight-hole holes-active-hole))
@@ -328,7 +324,7 @@ the span."
 
 (defun holes-clear-hole (hole)
   "Clear the HOLE."
-  (assert (holes-is-hole-p hole) t
+  (cl-assert (holes-is-hole-p hole) t
 	  "holes-clear-hole: %s is not a hole")
   (if (and (holes-active-hole-exist-p)
 	   (eq holes-active-hole hole))
@@ -363,11 +359,11 @@ Operate betwenn START and END if non nil."
 Or after the hole at pos if there is one (default pos=point).  If no
 hole found, return nil."
   (holes-map-holes
-   (lambda (h x) (and (holes-is-hole-p h) h)) buffer pos))
+   (lambda (h _) (and (holes-is-hole-p h) h)) buffer pos))
 
 (defun holes-next-after-active-hole ()
   "Internal."
-  (assert (holes-active-hole-exist-p) t
+  (cl-assert (holes-active-hole-exist-p) t
 	  "next-active-hole: no active hole")
   (holes-next (holes-active-hole-end-position)
 	      (holes-active-hole-buffer)))
@@ -441,7 +437,7 @@ goal(FIXME?).  Use `replace-active-hole' instead."
 Like `holes-replace-active-hole', but then sets the active hole to the
 following hole if it exists."
   (interactive)
-  (assert (holes-active-hole-exist-p) t
+  (cl-assert (holes-active-hole-exist-p) t
 	  "holes-replace-update-active-hole: no active hole")
   (if (holes-active-hole-exist-p)
       (let ((nxthole (holes-next-after-active-hole)))
@@ -560,9 +556,9 @@ Sets `holes-active-hole' to the next hole if it exists."
   "Move the point to current active hole (if any and if in current buffer).
 Destroy it and makes the next hole active if any."
   (interactive)
-  (assert (holes-active-hole-exist-p) nil "no active hole")
-  (assert (eq (current-buffer) (holes-active-hole-buffer)) nil
-	  "active hole not in this buffer")
+  (cl-assert (holes-active-hole-exist-p) nil "no active hole")
+  (cl-assert (eq (current-buffer) (holes-active-hole-buffer)) nil
+	     "active hole not in this buffer")
   (holes-goto-active-hole)
   (holes-delete-update-active-hole))
 
@@ -593,7 +589,7 @@ The LIMIT argument bounds the search; it is a buffer position.
   (let ((n 0))
     (save-excursion
       (while (re-search-backward holes-empty-hole-regexp limit t)
-	(incf n)
+	(cl-incf n)
 	(if (not (match-end 1))
 	    (holes-make-hole (match-beginning 0) (match-end 0))
 	  (holes-make-hole (match-beginning 1) (match-end 1))
@@ -625,12 +621,12 @@ If NOINDENT is non-nil, skip the indenting step.
 If ALWAYSJUMP is non-nil, jump to the first hole even if more than one."
   (unless noindent (save-excursion (indent-region pos (point) nil)))
   (let ((n (holes-replace-string-by-holes-backward pos)))
-    (case n
-      (0 nil)				; no hole, stay here.
-      (1
+    (pcase n
+      (`0 nil)				; no hole, stay here.
+      (`1
        (goto-char pos)
        (holes-set-point-next-hole-destroy)) ; if only one hole, go to it.
-      (t
+      (_
        (goto-char pos)
        (when alwaysjump (holes-set-point-next-hole-destroy))
        (unless (active-minibuffer-window) ; otherwise minibuffer gets hidden
@@ -727,10 +723,9 @@ it mean anyway?)
  o Cutting or pasting a hole will not produce new holes, and
 undoing on holes cannot make holes re-appear."
   nil " Holes" holes-mode-map
-  :group 'holes
   (if holes-mode
-      (add-hook 'skeleton-end-hook 'holes-skeleton-end-hook nil t)
-    (remove-hook 'skeleton-end-hook 'holes-skeleton-end-hook t)
+      (add-hook 'skeleton-end-hook #'holes-skeleton-end-hook nil t)
+    (remove-hook 'skeleton-end-hook #'holes-skeleton-end-hook t)
     (holes-clear-all-buffer-holes)))
 
 ;;;###autoload
diff --git a/lib/pg-dev.el b/lib/pg-dev.el
index 8e82a753..78d79862 100644
--- a/lib/pg-dev.el
+++ b/lib/pg-dev.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
@@ -24,9 +24,6 @@
 (require 'whitespace)
 
 (eval-when-compile
-  (require 'cl))
-
-(eval-when-compile
   (require 'proof-site))
 
 (with-no-warnings
diff --git a/lib/proof-compat.el b/lib/proof-compat.el
index 25c029c6..95c533e5 100644
--- a/lib/proof-compat.el
+++ b/lib/proof-compat.el
@@ -28,7 +28,7 @@
 
 ;;; Code:
 
-(require 'cl)
+(require 'cl-lib)
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;;
@@ -63,7 +63,7 @@ in the current Emacs session."
 	     saved-value
 	     theme-value
 	     theme-face))
-    (remprop symbol prop)))
+    (cl-remprop symbol prop)))
 
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
diff --git a/lib/span.el b/lib/span.el
index e7e3d68b..4bb7507e 100644
--- a/lib/span.el
+++ b/lib/span.el
@@ -1,9 +1,9 @@
-;;; span.el --- Datatype of "spans" for Proof General
+;;; span.el --- Datatype of "spans" for Proof General  -*- 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
@@ -24,8 +24,6 @@
 
 ;;; Code:
 
-(eval-when-compile (require 'cl))       ;For lexical-let.
-
 (defalias 'span-start 'overlay-start)
 (defalias 'span-end 'overlay-end)
 (defalias 'span-set-property 'overlay-put)
@@ -42,10 +40,9 @@
   "Check if an overlay OL belongs to PG."
   (overlay-get ol 'pg-span))
 
-(defun span-read-only-hook (overlay after start end &optional len)
+(defun span-read-only-hook (&rest _)
   (unless inhibit-read-only
-    (error "Region is read-only")))
-(add-to-list 'debug-ignored-errors "Region is read-only")
+    (user-error "Region is read-only")))
 
 (defun span-read-only (span)
   "Set SPAN to be read only."
@@ -61,12 +58,11 @@
 
 (defun span-write-warning (span fun)
   "Give a warning message when SPAN is changed, unless `inhibit-read-only' is non-nil."
-  (lexical-let ((fun fun))
-    (let ((funs (list (lambda (span afterp beg end &rest args)
-			(if (and (not afterp) (not inhibit-read-only))
-			    (funcall fun beg end))))))
-      (span-set-property span 'modification-hooks funs)
-      (span-set-property span 'insert-in-front-hooks funs))))
+  (let ((funs (list (lambda (_span afterp beg end &rest _)
+		      (if (and (not afterp) (not inhibit-read-only))
+			  (funcall fun beg end))))))
+    (span-set-property span 'modification-hooks funs)
+    (span-set-property span 'insert-in-front-hooks funs)))
 
 ;; We use end first because proof-locked-queue is often changed, and
 ;; its starting point is always 1
@@ -155,13 +151,13 @@ A span is before PT if it begins before the character before PT."
        (overlay-buffer span)
        (buffer-live-p (overlay-buffer span))))
 
-(defun span-raise (span)
-  "Set priority of SPAN to make it appear above other spans."
-  ;; FIXME: Emacs already uses a "shorter goes above" which takes care of
-  ;; preventing a span from seeing another.  So don't play with
-  ;; priorities, please!
-  ;; (span-set-property span 'priority 100)
-  )
+;; (defun span-raise (_span)
+;;   "Set priority of SPAN to make it appear above other spans."
+;;   ;; FIXME: Emacs already uses a "shorter goes above" which takes care of
+;;   ;; preventing a span from seeing another.  So don't play with
+;;   ;; priorities, please!
+;;   ;; (span-set-property span 'priority 100)
+;;   )
 
 (defun span-string (span)
   (with-current-buffer (overlay-buffer span)
@@ -180,7 +176,7 @@ A span is before PT if it begins before the character before PT."
         (overlays-at (posn-point (event-start event)))
         (or prop 'span))))
 
-(defun fold-spans (f &optional buffer from to maparg ignored-flags prop val)
+(defun fold-spans (f &optional buffer from to maparg _ignored-flags prop val)
   (with-current-buffer (or buffer (current-buffer))
     (let ((ols (overlays-in (or from (point-min)) (or to (point-max))))
           res)
@@ -238,7 +234,7 @@ The span will remove itself after a timeout of 2 seconds."
     (add-timeout 2 'delete-overlay ol)
     ol))
 
-(defun span-delete-self-modification-hook (span &rest args)
+(defun span-delete-self-modification-hook (span &rest _)
   "Hook for overlay modification-hooks, which deletes SPAN."
   (if (span-live-p span)
       (span-delete span)))
@@ -252,7 +248,7 @@ Return the span."
       (overlay-put ol (car props) (cadr props))
       (setq props (cddr props)))
     (span-set-property ol 'modification-hooks
-                       (list 'span-delete-self-modification-hook))
+                       (list #'span-delete-self-modification-hook))
     ol))
 
 
diff --git a/lib/texi-docstring-magic.el b/lib/texi-docstring-magic.el
index e39ee51a..2d6a3cf4 100644
--- a/lib/texi-docstring-magic.el
+++ b/lib/texi-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
@@ -92,9 +92,6 @@
 
 ;;; Code:
 
-(eval-when-compile
-  (require 'cl))
-
 (defun texi-docstring-magic-find-face (face)
   "Return non-nil if FACE is a face name; nil otherwise.
 A face name can be a string or a symbol.
diff --git a/lib/unicode-tokens.el b/lib/unicode-tokens.el
index 4d1d0d35..41f478d1 100644
--- a/lib/unicode-tokens.el
+++ b/lib/unicode-tokens.el
@@ -46,7 +46,7 @@
 
 ;;; Code:
 
-(require 'cl)
+(require 'cl-lib)
 (require 'quail)
 
 (eval-when-compile
@@ -429,12 +429,12 @@ This function also initialises the important tables for the mode."
     ;; hairy logic based on Coq-style vs Isabelle-style configs
     (if (string= "" (format unicode-tokens-token-format ""))
 	;; no special token format, parse separate words/symbols
- 	(let* ((tokextra (remove* "^\\(?:\\sw\\|\\s_\\)+$" toks :test 'string-match))
-               (toksymbwrd (set-difference toks tokextra))
+ 	(let* ((tokextra (cl-remove "^\\(?:\\sw\\|\\s_\\)+$" toks :test 'string-match))
+               (toksymbwrd (cl-set-difference toks tokextra))
                ;; indentifier that are not pure words
-               (toksymb (remove* "^\\(?:\\sw\\)+$" toksymbwrd :test 'string-match))
+               (toksymb (cl-remove "^\\(?:\\sw\\)+$" toksymbwrd :test 'string-match))
                ;; pure words
-               (tokwrd (set-difference toksymbwrd toksymb))
+               (tokwrd (cl-set-difference toksymbwrd toksymb))
 	       (idorop
 		(concat "\\(\\_<"
                         (regexp-opt toksymb)
@@ -461,9 +461,9 @@ This function also initialises the important tables for the mode."
 The check is with `char-displayable-p'."
   (cond
    ((stringp comp)
-    (reduce (lambda (x y) (and x (char-displayable-p y)))
- 	    comp
- 	    :initial-value t))
+    (cl-reduce (lambda (x y) (and x (char-displayable-p y)))
+ 	       comp
+ 	       :initial-value t))
    ((characterp comp)
     (char-displayable-p comp))
    (comp ;; assume any other non-null is OK
@@ -518,7 +518,7 @@ The face property is set to the :family and :slant attriubutes taken from
 					    (car props) (cadr props))
 	    (setq props (cddr props)))))
     (unless (or unicode-tokens-show-symbols
-		(intersection unicode-tokens-fonts propsyms))
+		(cl-intersection unicode-tokens-fonts propsyms))
       (font-lock-append-text-property
        start end 'face
        ;; just use family and slant to enhance merging with other faces
@@ -680,7 +680,7 @@ Calculated from `unicode-tokens-token-name-alist' and
 `unicode-tokens-shortcut-alist'."
   (let ((unicode-tokens-quail-define-rules
 	 (list 'quail-define-rules)))
-    (let ((ulist (copy-list unicode-tokens-shortcut-alist))
+    (let ((ulist (copy-sequence unicode-tokens-shortcut-alist))
 	  ustring shortcut)
       (setq ulist (sort ulist 'unicode-tokens-map-ordering))
       (while ulist
@@ -714,7 +714,7 @@ Available annotations chosen from `unicode-tokens-control-regions'."
 			"Annotate region with: "
 			unicode-tokens-control-regions nil
 			'requirematch))))
-  (assert (assoc name unicode-tokens-control-regions))
+  (cl-assert (assoc name unicode-tokens-control-regions))
   (let* ((entry (assoc name unicode-tokens-control-regions))
 	 (beg   (region-beginning))
 	 (end   (region-end))
@@ -736,7 +736,7 @@ Available annotations chosen from `unicode-tokens-control-regions'."
 		      "Insert control symbol: "
 		      unicode-tokens-control-characters
 		      nil 'requirematch)))
-  (assert (assoc name unicode-tokens-control-characters))
+  (cl-assert (assoc name unicode-tokens-control-characters))
   (insert (format unicode-tokens-control-char-format
 		  (cadr (assoc name unicode-tokens-control-characters)))))
 
@@ -833,7 +833,8 @@ but multiple characters in the underlying buffer."
 	    (error "Cannot find token before point"))
 	  (when token
 	    (let* ((tokennumber
-		    (search (list token) unicode-tokens-token-list :test 'equal))
+		    (cl-search (list token) unicode-tokens-token-list
+                               :test #'equal))
 		   (numtoks
 		    (hash-table-count unicode-tokens-hash-table))
 		   (newtok
@@ -943,7 +944,7 @@ Starts from point."
 			     'face
 			     'header-line))
 	    (insert " "))
-	  (incf count)
+	  (cl-incf count)
 	  (if (null toks)
 	      (insert " ")
 	    (insert-text-button
diff --git a/obsolete/plastic/plastic.el b/obsolete/plastic/plastic.el
index 09a61b27..cf69a731 100644
--- a/obsolete/plastic/plastic.el
+++ b/obsolete/plastic/plastic.el
@@ -13,8 +13,8 @@
 
 (require 'proof)
 
+(require 'cl-lib)                       ;cl-member-if
 (eval-when-compile
-  (require 'cl)
   (require 'span)
   (require 'proof-syntax)
   (require 'outline))
@@ -229,7 +229,7 @@ Given is the first SPAN which needs to be undone."
 	     (setq i 0)
 	     (while (< i (length string))
 	       (if (string-equal (substring string i (+ i tl)) proof-terminal-string)
-		   (incf ct))
+		   (cl-incf ct))
 	       (setq i (+ 1 i)))))
       (setq span (next-span span 'type)))
     (list (concat plastic-lit-string 
@@ -264,9 +264,9 @@ Given is the first SPAN which needs to be undone."
 	;	(list (concat "Can't Undo imports yet\n"
 	;			   "You have to exit Plastic for this\n")
 	;	      ["ok, I'll do this" (lambda () t) t]))
-	    (return)
+	    (cl-return)  ;FIXME: No enclosing block?!
 	   )    ;; warn the user that undo of imports not yet working.
-	 (t (incf spans))
+	 (t (cl-incf spans))
       )
       (setq span (next-span span 'type))
 
@@ -453,7 +453,7 @@ Value for `proof-shell-compute-new-files-list', which see.
 
 For Plastic, we assume that module identifiers coincide with file names."
   (let ((module (match-string 1)))
-    (cdr (member-if
+    (cdr (cl-member-if
 	  (lambda (filename) (plastic-equal-module-filename module filename))
 	  proof-included-files-list))))
 
@@ -541,33 +541,33 @@ For Plastic, we assume that module identifiers coincide with file names."
 	(l (length string))
 	(eat-rest (lambda ()
 		    (aset string i ?\ )  ;; kill the \n or "-" at least
-		    (incf i)
+		    (cl-incf i)
 		    (while (and (< i l) (/= (aref string i) ?\n))
 		      (aset string i ?\ )
-		      (incf i) )))
+		      (cl-incf i) )))
 	(keep-rest (lambda ()
 		     (loop for x in (string-to-list plastic-lit-string)
-		       do (aset string i ?\ ) (incf i))
+		       do (aset string i ?\ ) (cl-incf i))
 		     (while (and (< i l)
 				 (/= (aref string i) ?\n)
 				 (/= (aref string i) ?-))
-		       (incf i) ))))
+		       (cl-incf i) ))))
      (while (< i l)
        (cond
 	((eq 0 (string-match "--" (substring string i)))
 	 (funcall eat-rest))		; comment.
 	((eq 0 (string-match "\n\n" (substring string i)))
 	 (aset string i ?\ )
-	 (incf i))			; kill repeat \n
+	 (cl-incf i))			; kill repeat \n
 	((= (aref string i) ?\n)	; start of new line
-	 (aset string i ?\ ) (incf i)	; remove \n
+	 (aset string i ?\ ) (cl-incf i)	; remove \n
 	 (if (eq 0 (string-match plastic-lit-string
 				 (substring string i)))
 	     (funcall keep-rest)	; code line.
 	   (funcall eat-rest)		; non-code line
 	   ))
 	(t
-	 (incf i))))			; else include.
+	 (cl-incf i))))			; else include.
      (setq string (replace-regexp-in-string "  +" " " string))
      (setq string (replace-regexp-in-string "^ +" "" string))
    (if (string-match "^\\s-*$" string)