diff options
| author | Jason Gross | 2020-04-28 15:43:13 -0400 |
|---|---|---|
| committer | Jason Gross | 2020-05-02 13:20:54 -0400 |
| commit | 570dd44feec40ca2be2dd6a4d46ca5378acdce09 (patch) | |
| tree | f91db8f27407b764568743f459f3c588a01a9298 /doc/changelog | |
| parent | 1700c63e82c0b10cbdeda8d79639d925a7571e12 (diff) | |
LtacProf now handles multi-success backtracking
Fixes #12196
Diffstat (limited to 'doc/changelog')
| -rw-r--r-- | doc/changelog/05-tactic-language/12197-ltacprof-multi-success.rst | 8 |
1 files changed, 8 insertions, 0 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 new file mode 100644 index 0000000000..b90c8e7a1f --- /dev/null +++ b/doc/changelog/05-tactic-language/12197-ltacprof-multi-success.rst @@ -0,0 +1,8 @@ +- **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). |