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.

15 files changed, 109 insertions, 120 deletions

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