From 6234ecf5f5752768175d510749cc48a97c2c0dbe Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Mon, 12 Sep 2016 15:14:23 +0200
Subject: Refolding: disable in 8.4 compat file, document

---
 doc/refman/RefMan-tac.tex | 10 ++++++++++
 1 file changed, 10 insertions(+)

(limited to 'doc/refman')

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}
-- 
cgit v1.2.3