diff options
| -rw-r--r-- | doc/refman/RefMan-tac.tex | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index 5f38017b7c..b491cc3d40 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -1893,6 +1893,14 @@ introduced hypothesis. {\ident}}. \ErrMsg \errindex{goal does not satisfy the expected preconditions} + +\item \texttt{injection} \ident{} \texttt{as} \nelist{\intropattern}{}\\ +\texttt{injection} \num{} \texttt{as} {\intropattern} {\ldots} {\intropattern}\\ +\texttt{injection} \texttt{as} {\intropattern} {\ldots} {\intropattern}\\ +\tacindex{injection \ldots{} as} + +These variants apply \texttt{intros} \nelist{\intropattern}{} after the call to \texttt{injection}. + \end{Variants} \subsection{\tt simplify\_eq {\ident} |