From fa5d9b87b0ff4145193fce84c99a4b351cb32a1f Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 20 Jan 2012 23:52:13 +0000
Subject: Added documentation for "r foo" in Ltac debugger.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14931 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 doc/refman/RefMan-ltac.tex | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'doc')

diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex
index 38ad9aa86b..d7f00584e0 100644
--- a/doc/refman/RefMan-ltac.tex
+++ b/doc/refman/RefMan-ltac.tex
@@ -946,7 +946,8 @@ simple newline: & go to the next step\\
 h: & get help\\
 x: & exit current evaluation\\
 s: & continue current evaluation without stopping\\
-r$n$: & advance $n$ steps further\\
+r $n$: & advance $n$ steps further\\
+r {\qstring}: & advance up to the next call to ``{\tt idtac} {\qstring}''\\
 \end{tabular}
 \endinput
 
-- 
cgit v1.2.3