-*- 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.
*** New command `proof-check-report' to generates the proof status
    of all opaque proofs. Currently only available for Coq, see Coq
    changes below for more details.
*** New command `proof-check-annotate' to annotate all failing proofs
    with FAIL comments.
*** Don't ask about killing the proof assistant when quitting Emacs and
    thereby the Proof General session.
*** Improve splash screen, add menu entry to permanently disable it
    (Proof-General -> Quick Options -> Display -> Disable Splash Screen),
    reduce splash screen time to make it less annoying

** 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 command `proof-check-report to generates the proof status
    of all opaque proofs. This command is useful for a development
    process where invalid proofs are permitted and vos compilation and
    the omit proofs feature are used to work at the most interesting
    or challenging point instead of on the first invalid proof. The
    command generates a list of all opaque proofs in the current
    buffer together with the information whether the proof script is
    currently valid or invalid. The command can also be run in batch
    mode, for instance in a continuous integration environment.
*** New command `proof-check-annotate' to annotate all failing proofs
    with FAIL comments. Useful in the development process as described
    above to ensure all currently failing proofs are marked as such.
*** flag Printing Parentheses and Printing Notations can be set/unset
    via menu and Coq keymap (C-c C-a C-9 and C-c C-a C-0 for
    Parentheses (optimized for British and American keyboards); C-c
    C-a n and C-c C-a N for Notations).
*** 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.
*** Run Coq completely silent to fix #568. If you experience unexpected
    behavior, please report a bug and disable
    `coq-run-completely-silent' to switch back to old behavior. Note
    that external proof tree display is only supported if Coq/Rocq
    runs completely silent.
*** `Holes` library removed.
    This was a poor man's code template insertion. This is now removed
    and see next point below for a replacement.
*** yasnippets default code templates
    - if you use company-coq, this is disabled by default because
      company-coq uses its own yasnippet templates.
    - Templates are defined from coq-syntax.el definitions. No
      exhaustivity garanteed.
    - You might want to define your own templates instead.
    - To opt out from default templates:
          (setq coq-yasnippet-use-default-templates nil)
    - To out out from yasnippet with proofgeneral:
          (setq coq-use-yasnippet nil)

* Changes of Proof General 4.5 from Proof General 4.4
...
...
