Documenting the new Undo semantics

1 files changed, 1 insertions, 0 deletions

diff --git a/CHANGES b/CHANGES
index 8398853762..8fae9fb6f4 100644
--- a/CHANGES
+++ b/CHANGES
@@ -59,6 +59,7 @@ Vernacular commands
   Coq: terms, modules, tactics, etc. The old behaviour 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.
 
 Specification Language