diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2016-09-30 11:15:42 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2016-09-30 11:16:25 +0200 |
| commit | 215c4aaa5e4b51ff46f9dc536720af4c4ce9f5e8 (patch) | |
| tree | c4850a477c37071d7fe895894735925f9fdf9164 | |
| parent | 69d43e7615f080c2e4e57a87e84b51be857ab678 (diff) | |
| parent | b0a79d8c37267d2ba950dafb7094374910214eb3 (diff) | |
Merge remote-tracking branch 'github/pr/280' into v8.6
Was PR#280: Document that [Reset Ltac Profile] is not synchronized with
the document state
| -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 587f4e5cb..9378529cb 100644 --- a/doc/refman/RefMan-ltac.tex +++ b/doc/refman/RefMan-ltac.tex @@ -1289,7 +1289,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. |