diff options
Diffstat (limited to 'doc/changelog/04-tactics/11025-nativecompute-timing.rst')
| -rw-r--r-- | doc/changelog/04-tactics/11025-nativecompute-timing.rst | 11 |
1 files changed, 0 insertions, 11 deletions
diff --git a/doc/changelog/04-tactics/11025-nativecompute-timing.rst b/doc/changelog/04-tactics/11025-nativecompute-timing.rst deleted file mode 100644 index cb77457c31..0000000000 --- a/doc/changelog/04-tactics/11025-nativecompute-timing.rst +++ /dev/null @@ -1,11 +0,0 @@ -- **Changed:** The :flag:`NativeCompute Timing` flag causes calls to - :tacn:`native_compute` (as well as kernel calls to the native - compiler) to emit separate timing information about conversion to - native code, compilation, execution, and reification. It replaces - the timing information previously emitted when the `-debug` flag was - set, and allows more fine-grained timing of the native compiler - (`#11025 <https://github.com/coq/coq/pull/11025>`_, by Jason Gross). - Additionally, the timing information now uses real time rather than - user time (Fixes `#11962 - <https://github.com/coq/coq/issues/11962>`_, `#11963 - <https://github.com/coq/coq/pull/11963>`_, by Jason Gross) |