From 100d50d7cde05334940378a1e6483cae975b93a5 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 16 Feb 2015 11:30:24 +0100
Subject: Documenting "induction t in ctx" when ctx contains an hyp not
 mentioning t.

---
 doc/refman/RefMan-tac.tex | 16 +++++++++++++---
 1 file changed, 13 insertions(+), 3 deletions(-)

diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index ee40a0d51e..c2407dce2c 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -1789,9 +1789,19 @@ induction n.
 \item \texttt{induction {\term} in {\occgoalset}}
 
   This syntax is used for selecting which occurrences of {\term} the
-  induction has to be carried on. The {\tt in \occgoalset} clause is an
-  occurrence clause whose syntax and behavior is described in
-  Section~\ref{Occurrences_clauses}.
+  induction has to be carried on. The {\tt in \occgoalset} clause is
+  an occurrence clause whose syntax and behavior is described in
+  Section~\ref{Occurrences_clauses}. If variables or hypotheses not
+  mentioning {\term} in their type are listed in {\occgoalset}, those
+  are generalized as well in the statement to prove.
+
+\Example
+
+\begin{coq_example}
+Lemma comm x y : x + y = y + x.
+induction y in x |- *.
+Show 2.
+\end{coq_example}
 
 \item {\tt induction {\term$_1$} with {\bindinglist$_1$}
        as {\disjconjintropattern} %% eqn:{\namingintropattern}
-- 
cgit v1.2.3