[NonGNU ELPA] Proof-General version 4.5

[ELPA update]

Version 4.5 of package Proof-General has just been released in NonGNU ELPA.
You can now find it in M-x list-packages RET.

Proof-General describes itself as:

  ==============================================
  A generic Emacs interface for proof assistants
  ==============================================

More at https://elpa.nongnu.org/nongnu/proof-general.html

## Summary:

  Proof General is a generic Emacs interface for proof assistants
  (also known as interactive theorem provers).

  It is supplied ready to use for the proof assistants Coq,
  EasyCrypt, qrhl-tool, and PhoX.

  See https://proofgeneral.github.io/ for installation instructions
  and online documentation.  Or browse the accompanying info manual:
  (info-display-manual "ProofGeneral")

## Recent NEWS:

-*- outline -*-  

This is a summary of main changes.  For details, please see
the Git ChangeLog, the GitHub repo https://github.com/ProofGeneral/PG

* Changes of Proof General 4.6 from Proof General 4.5

** Generic changes
*** Improve the omit-proofs feature to handle a number of cases where
    proofs must not be omitted.
*** Renew support for proof-tree visualization via the external command
    prooftree, see http://askra.de/software/prooftree and Section 7
    "Graphical Proof-Tree Visualization" in the Proof General manual.
    Proof-tree visualization is currently only supported for Coq. The
    prooftree support has been substantially rewritten, making use of
    the much better support since Coq version 8.11.

** Coq changes
*** support Coq 8.19
**** New option coq-compile-coqdep-warnings to configure the warning
     command line argument (-w) of coqdep. The default of this option
     is +module-not-found to let Proof General reliably detect missing
     modules as coqdep error.
*** Renew support for proof-tree visualization, see description in
    generic changes above.


**** New options coq-compile-extra-coqc-arguments and
     coq-compile-extra-coqdep-arguments to configure additional
     command line arguments to calls of, respetively, coqc and coqdep
     during auto compilation.

**** Fix issues #687 and #688 where the omit-proofs feature causes
     errors on correct code.


* Changes of Proof General 4.5 from Proof General 4.4

** Generic changes
*** License changed to GPLv3+
*** Remove support for the following systems:
Twelf, CCC, Lego, Hol-Light, ACL2, Plastic, Lambda-Clam, Isabelle, HOL98.

*** require GNU Emacs 25.2 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). Support for Emacs 25 will
be dropped in April 2023 when Ubuntu Bionic reaches end of
standard support.


*** 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"
      or use the "Proof-General > Upgrade ELPA packages..." menu item

*** bug fixes
    - Using query-replace (or replace-string) in the processed region
      doesn't wrongly jump to the first match anymore.
    - cheat face (admit etc) now visible when locked.

*** remove key-binding for proof-electric-terminator-toggle
    - The default key-binding for proof-electric-terminator-toggle
      (C-c .) was too easy to enter by mistake. And it was not that
      useful as we can expect users to configure electric-terminator
      once and for all. Hence the removal of this default key-binding.

*** add another (fallback) key-binding for proof-goto-point
    - The default key-binding for proof-goto-point (C-c <C-return>)
      was not available in TTYs. Now, this function can also be run
      with "C-c RET", which happens to be automatically triggered if
      we type "C-c <C-return>" in a TTY.

*** new proof-priority-action-list
    Similar to proof-action-list, but holding actions that need
    to go to the proof assistant at the next opportunity.

** Qrhl-tool

   Support for qrhl-tool theorem prover has been added by Dominique
   Unruh.
   References:
   - Initial pull request: https://github.com/ProofGeneral/PG/pull/636
   - Qrhl-tool web site: https://dominique-unruh.github.io/qrhl-tool

** EasyCrypt

   Support for EasyCrypt has been added.

** Coq changes

*** fix highlighting issues for ssr tactics ending with colon

    Now, { exact: term. } will always be correctly highlighted.

    However, only (forall {T: Type}, Type) will be highlighted,
    unlike term (forall { T: Type }, Type) that has a spurious space.

    Also in (forall [T: Type], Type), variable T is now highlighted.

*** new menu Coq -> Auto Compilation for all background compilation options
...
...