diff options
author | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-02-01 18:10:49 +0000 |
---|---|---|
committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-02-01 18:10:49 +0000 |
commit | 81fd137b585ad8b78794267269556b5439be31f1 (patch) | |
tree | 0a869cf268f8eb2a9ebac415f94be3812372af2c | |
parent | dd82ad0407241b09a108c324a28207d8535b3bbb (diff) |
Report 9545 de 8.1 vers trunk
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9581 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r-- | doc/refman/RefMan-tac.tex | 33 |
1 files changed, 32 insertions, 1 deletions
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index b8aa0bd59..442f4fa83 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -702,7 +702,6 @@ This tactic applies to any goal. It implements the rule \end{Variants} \SeeAlso \ref{Conversion-tactics} - \subsection{Bindings list \index{Binding list} \label{Binding-list}} @@ -725,6 +724,36 @@ all the dependent products in the type of \term\ while in the case of {\tt apply} only the dependent products which are not bound in the conclusion of the type are given. +\subsection{\tt evar (\ident:\term) +\tacindex{evar} +\label{evar}} + +The {\tt evar} tactic creates a new local definition named \ident\ with +type \term\ in the context. The body of this binding is a fresh +existential variable. + +\subsection{\tt instantiate (\num:= \term) +\tacindex{instantiate} +\label{instantiate}} + +The {\tt instantiate} tactic allows to solve an existential variable +with the term \term. The \num\ argument is the position of the +existential variable from right to left in the conclusion. This cannot be +the number of the existential variable since this number is different +in every session. + +\begin{Variants} + \item {\tt instantiate (\num:=\term) in \ident} + + \item {\tt instantiate (\num:=\term) in (Value of \ident)} + + \item {\tt instantiate (\num:=\term) in (Type of \ident)} + +These allow to refer respectively to existential variables occurring in +a hypothesis or in the body or the type of a local definition. + +\end{Variants} + \section{Negation and contradiction} @@ -3150,6 +3179,8 @@ pattern-matching on hypotheses. % \item \texttt{Overriding hint named \dots\ in database \dots} %\end{Warnings} + + \subsection{Hint databases defined in the \Coq\ standard library} Several hint databases are defined in the \Coq\ standard library. The |