From 1d1d034f68116426508b53ecaaeab49bf2c9eb82 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Thu, 7 Jun 2007 15:59:09 +0000
Subject: Ajout doc clear sans argument

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9880 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 doc/refman/RefMan-tac.tex | 17 ++++++++++++-----
 1 file changed, 12 insertions(+), 5 deletions(-)

diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index cd3a786e7a..e93e504ada 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}
 
-- 
cgit v1.2.3