diff options
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/refman/RefMan-tac.tex | 16 |
1 files changed, 15 insertions, 1 deletions
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index 432ff52796..2382175601 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -822,6 +822,14 @@ introduction pattern~$p$: of the constructor of $I$ (observe that {\tt ($p_1$, {\ldots}, $p_n$)} is an alternative notation for {\tt [$p_1$ {\ldots} $p_n$]}); +\item as a special case, if the product is over an equality type, then + a pattern of the form {\tt [$p_{1}$ \dots\ $p_n$]} or of the form + {\tt ($p_1$, \ldots, $p_n$)} applies {\tt injection} instead of {\tt + destruct} on the hypothesis and use the patterns $p_1$, \ldots, + $p_n$ on the hypotheses generated by {\tt injection} (see + Section~\ref{injection}); if the number of patterns is smaller than + the number of hypotheses generated, the pattern \texttt{?} is used + to complete the list; \item introduction via {\tt ($p_1$ \& \dots\ \& $p_n$)} is a shortcut for introduction via {\tt ($p_1$,(\ldots,(\dots,$p_n$)\ldots))}; it expects the @@ -2118,7 +2126,13 @@ introduced hypothesis. \tacindex{injection \dots\ as} These variants apply \texttt{intros} \nelistnosep{\intropattern} after -the call to \texttt{injection} or \texttt{einjection}. +the call to \texttt{injection} or \texttt{einjection} so that all +equalities generated are moved in the context of hypotheses. The +number of {\intropattern} must not exceed the number of equalities +newly generated. If it is smaller, fresh names are automatically +generated to adjust the list of {\intropattern} to the number of new +equalities. The original equality is erased if it corresponds to an +hypothesis. \end{Variants} |