Merge branch 'v8.6'

2 files changed, 11 insertions, 1 deletions

diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex
index 9fbff7181e..1d89c17f47 100644
--- a/doc/refman/RefMan-ltac.tex
+++ b/doc/refman/RefMan-ltac.tex
@@ -1158,7 +1158,7 @@ using the syntax:
 \end{quote}
 A previous definition of {\qualid} must exist in the environment.
 The new definition will always be used instead of the old one and
-it goes accross module boundaries.
+it goes across module boundaries.
 
 If preceded by the keyword {\tt Local} the tactic definition will not
 be exported outside the current module.
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index b668239a6a..8172b57714 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -3293,6 +3293,16 @@ reduced to \texttt{S t}.
 
 \end{Variants}
 
+\begin{quote}
+\optindex{Refolding Reduction}
+{\tt Refolding Reduction}
+\end{quote}
+
+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.
+
 \subsection{\tt unfold \qualid}
 \tacindex{unfold}
 \label{unfold}