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