2 files changed, 18 insertions, 11 deletions
diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex
index 0a4d0ef9aa..3ed697d8be 100644
--- a/doc/refman/RefMan-ltac.tex
+++ b/doc/refman/RefMan-ltac.tex
@@ -156,6 +156,8 @@ is understood as
 & | & {\tt type\_term} {\term}\\
 & | & {\tt numgoals} \\
 & | & {\tt guard} {\it test}\\
+& | & {\tt assert\_fails} {\tacexprpref}\\
+& | & {\tt assert\_succeds} {\tacexprpref}\\
 & | & \atomictac\\
 & | & {\qualid} \nelist{\tacarg}{}\\
 & | & {\atom}
@@ -598,6 +600,22 @@ The experimental status of this tactic pertains to the fact if $v$ performs side
 
 \ErrMsg \errindex{This tactic has more than one success}
 
+\subsubsection[Checking the failure]{Checking the failure\tacindex{assert\_fails}\index{Tacticals!assert\_fails@{\tt assert\_fails}}}
+
+Coq provides a derived tactic to check that a tactic \emph{fails}:
+\begin{quote}
+{\tt assert\_fails} {\tacexpr}
+\end{quote}
+This behaves like {\tt tryif {\tacexpr} then fail 0 tac "succeeds" else idtac}.
+
+\subsubsection[Checking the success]{Checking the success\tacindex{assert\_succeeds}\index{Tacticals!assert\_succeeds@{\tt assert\_succeeds}}}
+
+Coq provides a derived tactic to check that a tactic has \emph{at least one} success:
+\begin{quote}
+{\tt assert\_succeeds} {\tacexpr}
+\end{quote}
+This behaves like {\tt tryif (assert\_fails tac) then fail 0 tac "fails" else idtac}.
+
 \subsubsection[Solving]{Solving\tacindex{solve}
 \index{Tacticals!solve@{\tt solve}}}
 
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index 40ba43b6cd..2597e3c37d 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -3505,17 +3505,6 @@ reduced to \texttt{S t}.
 \end{Variants}
 
 \begin{quote}
-\optindex{Refolding Reduction}
-{\tt Refolding Reduction}
-\end{quote}
-\emph{Deprecated since 8.7}
-
-This option (off by default) controls the use of the refolding strategy
-of {\tt cbn} while doing reductions in unification, type inference and
-tactic applications. It can result in expensive unifications, as
-refolding currently uses a potentially exponential heuristic.
-
-\begin{quote}
   \optindex{Debug RAKAM}
   {\tt Set Debug RAKAM}
 \end{quote}