From 8cee2c7ef9e15937fafe60ae43fec7c8bb3678c6 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Sun, 15 Feb 2015 16:59:37 +0100
Subject: Note about "Undo. Undo." in CHANGES

---
 CHANGES | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/CHANGES b/CHANGES
index dc7cfa90a7..8b4a4fc933 100644
--- a/CHANGES
+++ b/CHANGES
@@ -63,6 +63,8 @@ Vernacular commands
   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
-- 
cgit v1.2.3