Breakpoints in Ltac debugger: new command "r foo" to jump to the next

call to "idtac foo" in Ltac code.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14929 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 5 insertions, 0 deletions

diff --git a/CHANGES b/CHANGES
index cadfec6b8..1fd72f7b0 100644
--- a/CHANGES
+++ b/CHANGES
@@ -13,6 +13,11 @@ Vernacular commands
 - New command "Set Parsing Explicit" for deactivating parsing (and printing)
   of implicit arguments (useful for teaching).
 
+Tactics
+
+- New command "r string" that interprets "idtac string" as a breakpoint
+  and jumps to its next use in Ltac debugger.
+
 Changes from V8.3 to V8.4beta
 =============================