diff options
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/refman/RefMan-ltac.tex | 2 | ||||
| -rw-r--r-- | doc/refman/RefMan-tac.tex | 10 |
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} |