diff options
| -rw-r--r-- | doc/refman/RefMan-tac.tex | 15 |
1 files changed, 3 insertions, 12 deletions
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index 18bcd1af62..34b974381a 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -1249,18 +1249,9 @@ in the list of subgoals remaining to prove. introduction pattern (in particular, if {\intropattern} is {\ident}, the tactic behaves like \texttt{assert ({\ident} :\ {\form})}). - If {\intropattern} is a disjunctive/conjunctive - introduction pattern, the tactic behaves like \texttt{assert - {\form}} followed by a {\tt destruct} using this introduction pattern. - - If {\intropattern} is a rewriting intropattern pattern, the tactic - behaves like \texttt{assert {\form}} followed by a call to {\tt - subst} on the resulting hypothesis, if applicable, or to {\tt - rewrite} otherwise. - - If {\intropattern} is an injection intropattern pattern, the tactic - behaves like \texttt{assert {\form}} followed by {\tt injection} - using this introduction pattern. + If {\intropattern} is an action introduction pattern, the tactic + behaves like \texttt{assert {\form}} followed by the action done by + this introduction pattern. \item \texttt{assert {\form} as {\intropattern} by {\tac}} |