MAJ manuel de référence

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8995 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 36 insertions, 1 deletions

diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index 2798c44ee..d9e600784 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -69,6 +69,13 @@ convertible (see Section~\ref{conv-rules}).
 \item \errindex{Not an exact proof}
 \end{ErrMsgs}
 
+\begin{Variants}
+  \item \texttt{eexact \term}\tacindex{eexact} 
+    
+    This tactic behaves like \texttt{exact} but is able to handle terms with meta-variables. 
+
+\end{Variants}
+
 
 \subsection{\tt refine \term
 \tacindex{refine}
@@ -112,6 +119,15 @@ subgoal is proved. Otherwise, it fails.
 \item  \errindex{No such assumption}
 \end{ErrMsgs}
 
+\begin{Variants}
+  \item \texttt{eassumption}
+
+    This tactic behaves like \texttt{assumption} but is able to handle
+    goals with meta-variables.
+
+\end{Variants}
+
+
 \subsection{\tt clear {\ident}
 \tacindex{clear}
 \label{clear}}
@@ -506,6 +522,11 @@ in the list of subgoals remaining to prove.
   following subgoals: {\tt U -> T} and \texttt{U}.  The subgoal {\tt U
     -> T} comes first in the list of remaining subgoal to prove.
 
+\item \texttt{assert {\form} by {\tac}}\tacindex{assert by}
+  
+  This tactic behaves like \texttt{assert} but tries to apply {\tac}
+  to any subgoals generated by \texttt{assert}.
+
 \end{Variants}
 
 % PAS CLAIR;
@@ -1012,6 +1033,14 @@ equivalent to {\tt intros; apply ci}.
     these expressions are equivalent to the corresponding {\tt
     constructor $i$ with \bindinglist}.
 
+\item \texttt{econstructor}
+
+  This tactic behaves like \texttt{constructor} but is able to
+  introduce existential variables if an instanciation for a variable
+  cannot be found (cf \texttt{eapply}). The tactics \texttt{eexists},
+  \texttt{esplit}, \texttt{eleft} and \texttt{eright} follows the same
+  behaviour.
+
 \end{Variants}
 
 \section{Eliminations (Induction and Case Analysis)}
@@ -1323,7 +1352,8 @@ inductive type with a single constructor.
 Lemma intros_test : forall A B C:Prop, A \/ B /\ C -> (A -> C) -> C.
 intros A B C [a| [_ c]] f.
 apply (f a).
-Proof c.
+exact c.
+Qed.
 \end{coq_example}
 
 %\subsection{\tt FixPoint \dots}\tacindex{Fixpoint}
@@ -2166,6 +2196,11 @@ hints of the database named {\tt core}.
   Uses all existing hint databases, minus the special database
   {\tt v62}. See Section~\ref{Hints-databases}
 
+\item \texttt{auto using $lemma_1, \ldots, lemma_n$}
+
+  Uses $lemma_1, \ldots, lemma_n$ in addition to hints (can be conbined
+  with the \texttt{with \ident} option).
+
 \item {\tt trivial}\tacindex{trivial}
 
   This tactic is a restriction of {\tt auto} that is not recursive and