From 570dd44feec40ca2be2dd6a4d46ca5378acdce09 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 28 Apr 2020 15:43:13 -0400 Subject: LtacProf now handles multi-success backtracking Fixes #12196 --- doc/changelog/05-tactic-language/12197-ltacprof-multi-success.rst | 8 ++++++++ 1 file changed, 8 insertions(+) create mode 100644 doc/changelog/05-tactic-language/12197-ltacprof-multi-success.rst (limited to 'doc/changelog') 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 + `_, `#12197 + `_, by Jason Gross). -- cgit v1.2.3