Merge branch 'v8.5'

1 files changed, 0 insertions, 3 deletions

diff --git a/CHANGES b/CHANGES
index 8b4a4fc933..19da2a4c81 100644
--- a/CHANGES
+++ b/CHANGES
@@ -62,9 +62,6 @@ Vernacular commands
   Coq: terms, modules, tactics, etc. The old behavior of the command can be
   retrieved using the "Locate Term" command.
 - New "Derive" command to help writing program by derivation.
-- "Undo" undoes any command, not just tactics.
-- "Undo. Undo." does not work in CoqIDE or Proof General, it works only
-  in coqtop.  "Undo 2" should be used intead.
 - New "Refine Instance Mode" option that allows to deactivate the generation of
   obligations in incomplete typeclass instances, raising an error instead.
 - "Collection" command to name sets of section hypotheses.  Named collections