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/sphinx/proof-engine/ltac.rst | 18 ++++++++++++------
 1 file changed, 12 insertions(+), 6 deletions(-)

(limited to 'doc/sphinx/proof-engine')

diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst
index c1eb1f974c..faa44adaf6 100644
--- a/doc/sphinx/proof-engine/ltac.rst
+++ b/doc/sphinx/proof-engine/ltac.rst
@@ -1778,16 +1778,22 @@ performance issue.
    and allow displaying and resetting the profile from tactic scripts for
    benchmarking purposes.
 
+.. warn:: Ltac Profiler encountered an invalid stack (no \
+         self node). This can happen if you reset the profile during \
+         tactic execution
+
+   Currently, :tacn:`reset ltac profile` is not very well-supported,
+   as it clears all profiling information about all tactics, including
+   ones above the current tactic.  As a result, the profiler has
+   trouble understanding where it is in tactic execution.  This mixes
+   especially poorly with backtracking into multi-success tactics.  In
+   general, non-top-level calls to :tacn:`reset ltac profile` should
+   be avoided.
+
 You can also pass the ``-profile-ltac`` command line option to ``coqc``, which
 turns the :flag:`Ltac Profiling` flag on at the beginning of each document,
 and performs a :cmd:`Show Ltac Profile` at the end.
 
-.. warning::
-
-   Note that the profiler currently does not handle backtracking into
-   multi-success tactics, and issues a warning to this effect in many cases
-   when such backtracking occurs.
-
 Run-time optimization tactic
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
-- 
cgit v1.2.3