Granting Jason's request for an ad hoc compatibility option on

considering trivial unifications "?x = t" in tactics working under
conjunctions (see #3545).

Also updating and fixing wrong comments in test apply.v.

1 files changed, 17 insertions, 0 deletions

diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index cc262708a..fa6f78393 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -485,7 +485,24 @@ apply Rmp.
 Reset R.
 \end{coq_eval}
 
+\noindent {\bf Remark: } When the conclusion of the type of the term
+to apply is an inductive type isomorphic to a tuple type and {\em apply}
+looks recursively whether a component of the tuple matches the goal,
+it excludes components whose statement would result in applying an
+universal lemma of the form {\tt forall A, ... -> A}. Excluding this
+kind of lemma can be avoided by setting the following option:
+
+\begin{quote}
+\optindex{Universal Lemma Under Conjunction}
+{\tt Set Universal Lemma Under Conjunction}
+\end{quote}
+
+This option, which preserves compatibility with versions of {\Coq}
+prior to 8.4 is also available for {\tt apply {\term} in {\ident}}
+(see Section~\ref{apply-in}).
+
 \subsection{\tt apply {\term} in {\ident}}
+\label{apply-in}
 \tacindex{apply \dots\ in}
 
 This tactic applies to any goal.  The argument {\term} is a term