From 81fd137b585ad8b78794267269556b5439be31f1 Mon Sep 17 00:00:00 2001
From: herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Thu, 1 Feb 2007 18:10:49 +0000
Subject: 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
---
 doc/refman/RefMan-tac.tex | 33 ++++++++++++++++++++++++++++++++-
 1 file changed, 32 insertions(+), 1 deletion(-)

(limited to 'doc/refman/RefMan-tac.tex')

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
-- 
cgit v1.2.3