diff options
Diffstat (limited to 'doc/changelog/05-tactic-language/12197-ltacprof-multi-success.rst')
| -rw-r--r-- | doc/changelog/05-tactic-language/12197-ltacprof-multi-success.rst | 8 |
1 files changed, 0 insertions, 8 deletions
diff --git a/doc/changelog/05-tactic-language/12197-ltacprof-multi-success.rst b/doc/changelog/05-tactic-language/12197-ltacprof-multi-success.rst deleted file mode 100644 index b90c8e7a1f..0000000000 --- a/doc/changelog/05-tactic-language/12197-ltacprof-multi-success.rst +++ /dev/null @@ -1,8 +0,0 @@ -- **Fixed:** - The :flag:`Ltac Profiling` machinery now correctly handles - backtracking into multi-success tactics. The call-counts of some - tactics are unfortunately inflated by 1, as some tactics are - implicitly implemented as :g:`tac + fail`, which has two - entry-points rather than one (Fixes `#12196 - <https://github.com/coq/coq/issues/12196>`_, `#12197 - <https://github.com/coq/coq/pull/12197>`_, by Jason Gross). |