From 054505fffac27409d6c0f613337f9cfd7e5c36ba Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Sun, 29 Mar 2020 22:18:42 -0400
Subject: NativeCompute Timing: Use real, not user time

User time is unreliable for `native_compute`.

Also output time spent in conversion to native code, just in case that
is ever slow.

Note that this also removes spurious newlines in the output.

Fixes #11962
---
 doc/sphinx/proof-engine/tactics.rst | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

(limited to 'doc/sphinx/proof-engine')

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
 
-- 
cgit v1.2.3