From b3d372c410e3dfffe5183632d1fe17917a829b9a Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Wed, 7 Sep 2016 15:17:29 -0700
Subject: Fix a typo in the reference manual

---
 doc/refman/RefMan-ltac.tex | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'doc')

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


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')

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