diff options
author | 2006-07-03 15:35:56 +0000 | |
---|---|---|
committer | 2006-07-03 15:35:56 +0000 | |
commit | ab8b2969dc3c7f7f61ae426bfb64dc05876535d7 (patch) | |
tree | 430c69afa336ddadfbf2ab9b05fcca0b7c7fe933 | |
parent | 1b20c96f8a64f2c1dd102c7a267bee946eb55e93 (diff) |
MAJ manuel de référence
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8995 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r-- | doc/refman/RefMan-tac.tex | 37 |
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 |