diff options
| author | herbelin | 2006-10-04 11:46:08 +0000 |
|---|---|---|
| committer | herbelin | 2006-10-04 11:46:08 +0000 |
| commit | 3a091f4a3342b7436558606180852af8f9e135ff (patch) | |
| tree | c52b137f89ef58e459e893cb9b6085e3f14b8388 | |
| parent | 91e4438e1a78feb85a186adfca853d3716e37335 (diff) | |
Doc injection as
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9202 85f007b7-540e-0410-9357-904b9bb8a0f7
| -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} |