diff options
author | 2009-10-08 13:39:01 +0000 | |
---|---|---|
committer | 2009-10-08 13:39:01 +0000 | |
commit | 93b74b4be215bd08ca7a123505177d6ec8ac7b4c (patch) | |
tree | cc5b80a8ba038a7c531afae977234f2afdc70699 /doc | |
parent | bdec9fddcdaa13800e04e718ffa52f87bddc52d9 (diff) |
Init/Tactics.v: tactic with nicer name 'exfalso' for 'elimtype False'
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12380 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'doc')
-rw-r--r-- | doc/refman/RefMan-tac.tex | 9 |
1 files changed, 9 insertions, 0 deletions
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index 6dbdaedd4..01816a396 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -1115,6 +1115,15 @@ the following way: \item {\tt H: A $\vd$ $\neg$B} \ becomes \ {\tt H: B $\vd$ $\neg$A} \end{itemize} +\subsection{\tt exfalso} +\label{exfalso} +\tacindex{exfalso} + +This tactic implements the ``ex falso quodlibet'' logical principle: +an elimination of {\tt False} is performed on the current goal, and the +user is then required to prove that {\tt False} is indeed provable in +the current context. This tactic is a macro for {\tt elimtype False}. + \section{Conversion tactics \index{Conversion tactics} \label{Conversion-tactics}} |