From 5653be43f7b21347896afd78954387fa1efcabc8 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Thu, 11 Apr 2002 14:24:41 +0000
Subject: Ajout Rename et Pose

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

(limited to 'doc')

diff --git a/doc/RefMan-tac.tex b/doc/RefMan-tac.tex
index 28307b4f35..d5da2e3202 100644
--- a/doc/RefMan-tac.tex
+++ b/doc/RefMan-tac.tex
@@ -197,6 +197,17 @@ then all hypotheses between {\ident$_1$} and {\ident$_2$} which
                    it depends on {\ident$_2$}}
 \end{ErrMsgs}
 
+\subsection{\tt Rename {\ident$_1$} into {\ident$_2$}.}\tacindex{Rename}
+This renames hypothesis {\ident$_1$} into {\ident$_2$} in the current
+context\footnote{but it does not rename the hypothesis in the
+proof-term...}
+
+\begin{ErrMsgs}
+\item \errindex{No such assumption}
+
+\item \errindex{{\ident$_2$} is already used}
+\end{ErrMsgs}
+
 \subsection{\tt Intro}
 \tacindex{Intro}
 \label{Intro}
@@ -404,6 +415,16 @@ which should not be substituted.
 This is the general form. It substitutes {\term} at occurrences
 {\num$_1^i$} \dots\ {\num$_{n_i}^i$} of hypothesis {\ident$_i$}. One
 of the {\ident}'s may be the word {\tt Goal}.
+
+\item{\tt Pose {\ident} := {\term}}\tacindex{Pose}\\
+  This adds the local definition {\ident} := {\term} to the current
+  context without performing any replacement in the goal or in the
+  hypotheses.
+
+\item{\tt Pose {\term}}\\
+  This behaves as {\tt Pose {\ident} := {\term}} but {\ident} is
+  generated by {\Coq}.
+
 \end{Variants}
 
 \subsection{\tt Assert {\ident} : {\form}}\tacindex{Assert}
-- 
cgit v1.2.3