diff options
author | 2007-06-07 15:59:09 +0000 | |
---|---|---|
committer | 2007-06-07 15:59:09 +0000 | |
commit | 1d1d034f68116426508b53ecaaeab49bf2c9eb82 (patch) | |
tree | 3111f53ec9832aa2695063fa101d1c1b8035a4f5 | |
parent | cfe8a58952105ce13231ff4a547b04cae48b7e66 (diff) |
Ajout doc clear sans argument
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9880 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r-- | doc/refman/RefMan-tac.tex | 17 |
1 files changed, 12 insertions, 5 deletions
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index cd3a786e7..e93e504ad 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -139,20 +139,27 @@ usable in the proof development. \begin{Variants} -\item {\tt clear {\ident$_1$} {\ldots} {\ident$_n$}.} +\item {\tt clear {\ident$_1$} {\ldots} {\ident$_n$}} This is equivalent to {\tt clear {\ident$_1$}. {\ldots} clear {\ident$_n$}.} -\item {\tt clearbody {\ident}.}\tacindex{clearbody} - +\item {\tt clearbody {\ident}}\tacindex{clearbody} + This tactic expects {\ident} to be a local definition then clears its body. Otherwise said, this tactic turns a definition into an assumption. -\item \texttt{clear - {\ident}.} +\item \texttt{clear - {\ident$_1$} {\ldots} {\ident$_n$}} + + This tactic clears all hypotheses except the ones depending in + the hypotheses named {\ident$_1$} {\ldots} {\ident$_n$} and in the + goal. + +\item \texttt{clear} - This tactic clears all hypotheses except the ones depending in {\ident}. + This tactic clears all hypotheses except the ones depending in + goal. \end{Variants} |