diff options
| author |  Jason Gross <jgross@mit.edu> | 2016-05-13 17:57:06 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2016-06-05 22:09:40 -0400 |
| commit | 739ead8b2d70f978e31f793234d7a633636742a1 (patch) | |
| tree | 15da3b48ea04a45333dbe6484f4f47badb912d35 /doc | |
| parent | 51b32595081d279624c8ec162f9ed686ed660d9b (diff) | |
-profileltac -> -profile-ltac, as per @herbelin
https://github.com/coq/coq/pull/150#issuecomment-219141596
```bash
git grep --name-only profileltac | xargs sed s'/profileltac/profile-ltac/g' -i
```
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. |