proof-undo-and-delete-last-successful-command does not meet spec

[Erik Martin-Dorel]

Hello,

I have just noticed the ProofGeneral function proof-undo-and-delete-last-successful-command does not really meet the specification that is described in its documentation, namely:

... the deleted command is put into the Emacs kill ring, so
you can use the usual `yank' and similar commands to retrieve the
deleted text.

I have performed a few tests and it seems sufficient to replace

(proof-undo-last-successful-command-1 'delete-region)

with

(proof-undo-last-successful-command-1 'kill-region)

in generic/pg-user.el to provide the missing feature.

Kind regards,

Erik Martin-Dorel

[David Aspinall]

Fixed, many thanks for the report.