From 2418cf8d5ff6f479a5b43a87c861141bf9067507 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 31 Jul 2015 21:31:37 +0200
Subject: 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.
---
 doc/refman/RefMan-tac.tex | 17 +++++++++++++++++
 1 file changed, 17 insertions(+)

(limited to 'doc')

diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index cc262708ab..fa6f783934 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
-- 
cgit v1.2.3