Add Set NativeCompute Timing

The command `Set NativeCompute Timing` causes calls to `native_compute`
(as well as kernel calls to the native compiler) to emit separate timing
information about compilation, execution, and reification.  This allows
more fine-grained timing of the native compiler without needing to set
the `-debug` flag.

1 files changed, 6 insertions, 0 deletions

diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst
index 53cfb973d4..36a5916868 100644
--- a/doc/sphinx/proof-engine/tactics.rst
+++ b/doc/sphinx/proof-engine/tactics.rst
@@ -3113,6 +3113,12 @@ the conversion in hypotheses :n:`{+ @ident}`.
    compilation cost is higher, so it is worth using only for intensive
    computations.
 
+   .. 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.
+
    .. flag:: NativeCompute Profiling
 
       On Linux, if you have the ``perf`` profiler installed, this flag makes