diff options
Diffstat (limited to 'doc/refman/RefMan-tac.tex')
| -rw-r--r-- | doc/refman/RefMan-tac.tex | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index 8172b5771..65b49893b 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -1491,10 +1491,10 @@ the local context. \tacindex{contradiction} This tactic applies to any goal. The {\tt contradiction} tactic -attempts to find in the current context (after all {\tt intros}) one -hypothesis that is equivalent to {\tt False}. It permits to prune -irrelevant cases. This tactic is a macro for the tactics sequence -{\tt intros; elimtype False; assumption}. +attempts to find in the current context (after all {\tt intros}) an +hypothesis that is equivalent to an empty inductive type (e.g. {\tt + False}), to the negation of a singleton inductive type (e.g. {\tt + True} or {\tt x=x}), or two contradictory hypotheses. \begin{ErrMsgs} \item \errindex{No such assumption} |