From b0a79d8c37267d2ba950dafb7094374910214eb3 Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Fri, 16 Sep 2016 12:16:52 -0700
Subject: Doc: [Reset Ltac Profile] is not synchronized

---
 doc/refman/RefMan-ltac.tex | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex
index 1d89c17f47..822f8a2227 100644
--- a/doc/refman/RefMan-ltac.tex
+++ b/doc/refman/RefMan-ltac.tex
@@ -1279,7 +1279,7 @@ Prints a profile for all tactics that start with {\qstring}. Append a period (.)
 \begin{quote}
 {\tt Reset Ltac Profile}.
 \end{quote}
-Resets the profile, that is, deletes all accumulated information
+Resets the profile, that is, deletes all accumulated information.  Note that backtracking across a {\tt Reset Ltac Profile} will not restore the information.
 
 \begin{coq_eval}
 Reset Initial.
-- 
cgit v1.2.3