diff options
Diffstat (limited to 'doc/sphinx')
| -rw-r--r-- | doc/sphinx/proof-engine/tactics.rst | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index 6a280b74c2..7da453b7af 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -3134,8 +3134,10 @@ the conversion in hypotheses :n:`{+ @ident}`. .. flag:: NativeCompute Timing This flag causes all calls to the native compiler to print - timing information for the compilation, execution, and - reification phases of native compilation. + timing information for the conversion to native code, + compilation, execution, and reification phases of native + compilation. Timing is printed in units of seconds of + wall-clock time. .. flag:: NativeCompute Profiling |