diff options
Diffstat (limited to 'doc')
| -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 59015742e..24f4b2a77 100644 --- a/doc/refman/RefMan-ltac.tex +++ b/doc/refman/RefMan-ltac.tex @@ -1272,7 +1272,7 @@ The following two tactics behave like {\tt idtac} but enable and disable the pro {\tt stop profiling}. \end{quote} -You can also pass the {\tt -profileltac} command line option to {\tt coqc}, which performs a {\tt Start Profiling} at the beginning of each document, and a {\tt Show Profile} at the end. +You can also pass the {\tt -profile-ltac} command line option to {\tt coqc}, which performs a {\tt Start Profiling} at the beginning of each document, and a {\tt Show Profile} at the end. Note that the profiler currently does not handle backtracking into multi-success tactics, and issues a warning to this effect in many cases when such backtracking occurs. |