[nongnu] elpa/proof-general cc5bfd0 5/5: Merge pull request #506 from ProofGeneral/fix-details

[ELPA Syncer]

branch: elpa/proof-general
commit cc5bfd0b5524313313c8e394656cdb5321b62a42
Merge: e2ee96b 055be0e
Author: Erik Martin-Dorel <erik@martin-dorel.org>
Commit: GitHub <noreply@github.com>

    Merge pull request #506 from ProofGeneral/fix-details
    
    Require Emacs 25.1 & Update CI config
---
 .github/workflows/test.yml |  4 ++--
 CHANGES                    |  9 +++++++++
 COMPATIBILITY              | 20 ++++++--------------
 README.md                  |  2 +-
 coq/coq.el                 |  2 --
 doc/ProofGeneral.texi      |  2 +-
 proof-general-pkg.el       |  2 +-
 proof-general.el           |  2 +-
 8 files changed, 21 insertions(+), 22 deletions(-)

diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml
index 8bb9f2b..7fcc473 100644
--- a/.github/workflows/test.yml
+++ b/.github/workflows/test.yml
@@ -17,8 +17,6 @@ jobs:
     strategy:
       matrix:
         emacs_version:
-          - 24.5
-          # 24.5 to be removed at End-of-Support of Ubuntu 16.04 LTS 
(https://wiki.ubuntu.com/Releases)
           - 25.1
           - 25.2
           - 25.3
@@ -93,6 +91,8 @@ jobs:
           - '8.9'
           - '8.10'
           - '8.11'
+          - '8.12'
+          - '8.13'
         ocaml_version:
           - minimal
       # at most 20 concurrent jobs per free account
diff --git a/CHANGES b/CHANGES
index da89b3a..56232b3 100644
--- a/CHANGES
+++ b/CHANGES
@@ -8,6 +8,15 @@ and the PG Trac http://proofgeneral.inf.ed.ac.uk/trac
 
 ** Generic changes
 
+*** require GNU Emacs 25.1 or later
+
+The current policy aims at supporting multiple Emacs versions,
+including those available in distributions Debian Stable
+(https://packages.debian.org/stable/emacs) and Ubuntu LTS
+(https://packages.ubuntu.com/emacs), until their End-Of-Support (see
+also https://wiki.ubuntu.com/Releases).
+
+
 *** new command and menu item to easily upgrade all packages
     - To upgrade all ELPA packages (including ProofGeneral if it was
       installed via MELPA), do "M-x proof-upgrade-elpa-packages RET"
diff --git a/COMPATIBILITY b/COMPATIBILITY
index e2345a9..ba7a6c2 100644
--- a/COMPATIBILITY
+++ b/COMPATIBILITY
@@ -4,12 +4,13 @@ Compatibility of Proof General
 This version of Proof General has been tested with these Emacs versions
 on recent Linux systems:
 
- Emacs 24.5          -- recommended and supported
- Emacs 24.3, 24.4    -- previous versions, should work
- Emacs 25 (dev)      -- next version, should work
- Emacs 23.2, earlier -- obsolete versions, do NOT work
+ Emacs 25.1          -- minimal supported version
+ Emacs 24.5, earlier -- previous versions, do NOT work
 
-and (main) prover versions:  Coq 8.4, Coq 8.5
+and (main) prover versions:
+
+  Coq 8.9, 8.10, 8.11, 8.12, 8.13 -- tested versions in PG's CI
+  Coq 8.4, 8.5, 8.6, 8.7, 8.8     -- previous versions, should work
 
 See below for notes about other operating systems.
 
@@ -43,12 +44,3 @@ For tips, please see here:
 Note that Windows compatibility isn't tested by the maintainers.  If
 you discover problems, please add notes on the Wiki page above, and
 submit patches to http://proofgeneral.inf.ed.ac.uk/trac
-
-
-
-
-
-
-
-
-
diff --git a/README.md b/README.md
index 0a78ab9..5972656 100644
--- a/README.md
+++ b/README.md
@@ -27,7 +27,7 @@ Two editions of Proof General are currently available:
 
 ## Installing Proof General
 
-Proof General requires GNU Emacs `24.5` or later.
+Proof General requires GNU Emacs `25.1` or later.
 
 The current policy aims at supporting multiple Emacs versions,
 including those available in [Debian 
Stable](https://packages.debian.org/stable/emacs)
diff --git a/coq/coq.el b/coq/coq.el
index 20238da..84708c1 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -126,8 +126,6 @@ Namely, goals that do not fit in the goals window."
    '("Set Suggest Proof Using. ") coq-user-init-cmd)
   "Command to initialize the Coq Proof Assistant.")
 
-
-(require 'coq-syntax)
 ;; FIXME: Even if we don't use coq-indent for indentation, we still need it for
 ;; coq-script-parse-cmdend-forward/backward and coq-find-real-start.
 (require 'coq-indent)
diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi
index bbd2515..69027ee 100644
--- a/doc/ProofGeneral.texi
+++ b/doc/ProofGeneral.texi
@@ -58,7 +58,7 @@
 @c
 
 @set version 4.5-git
-@set emacsversion 24.5
+@set emacsversion 25.1
 @set last-update February 2021
 @set rcsid $Id$
 
diff --git a/proof-general-pkg.el b/proof-general-pkg.el
index 7dd7fb6..eb84269 100644
--- a/proof-general-pkg.el
+++ b/proof-general-pkg.el
@@ -1,3 +1,3 @@
 (define-package "proof-general" "4.5-git"
   "A generic front-end for proof assistants (interactive theorem provers)"
-  '((emacs "24.5")))
+  '((emacs "25.1")))
diff --git a/proof-general.el b/proof-general.el
index 1603290..425ee60 100644
--- a/proof-general.el
+++ b/proof-general.el
@@ -11,7 +11,7 @@
 
 ;; Authors: (see the AUTHORS file distributed along the sources)
 ;; URL: https://proofgeneral.github.io/
-;; Package-Requires: ((emacs "24.5"))
+;; Package-Requires: ((emacs "25.1"))
 ;; Version: 4.5-git
 
 ;; This software is free software; you can redistribute it and/or