diff options
| author | Jason Gross | 2016-09-16 12:16:52 -0700 |
|---|---|---|
| committer | GitHub | 2016-09-16 12:16:52 -0700 |
| commit | b0a79d8c37267d2ba950dafb7094374910214eb3 (patch) | |
| tree | 1cf7c7d73621f2a6ac845f5e5eb85d847d9c348f | |
| parent | e6eef565639fb3840dd235eb675ece6e4dbeb082 (diff) | |
Doc: [Reset Ltac Profile] is not synchronized
| -rw-r--r-- | doc/refman/RefMan-ltac.tex | 2 |
1 files changed, 1 insertions, 1 deletions
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. |