From e4645ad6e7b42925ef34a7078c4e8175a4e7be6e Mon Sep 17 00:00:00 2001 From: herbelin Date: Mon, 1 Mar 2004 16:21:13 +0000 Subject: Ajout 'replace in' git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8485 85f007b7-540e-0410-9357-904b9bb8a0f7 --- doc/RefMan-tac.tex | 23 ++++++++++++----------- 1 file changed, 12 insertions(+), 11 deletions(-) (limited to 'doc') diff --git a/doc/RefMan-tac.tex b/doc/RefMan-tac.tex index 565c94e6a..1673ceb88 100644 --- a/doc/RefMan-tac.tex +++ b/doc/RefMan-tac.tex @@ -1443,17 +1443,18 @@ equality {\term$_2$}{\tt =}{\term$_1$} as a subgoal. It is equivalent to {\tt cut \term$_2$=\term$_1$; intro H{\sl n}; rewrite <- H{\sl n}; clear H{\sl n}}. -%N'existe pas... -%\begin{Variants} -% -%\item {\tt replace {\term$_1$} with {\term$_2$} in \ident} -% This replaces {\term$_1$} with {\term$_2$} in the hypothesis named -% \ident, and generates the subgoal {\term$_2$}{\tt =}{\term$_1$}. -% \begin{ErrMsgs} -% \item \errindex{No such hypothesis} -% \end{ErrMsgs} -% -%\end{Variants} +\begin{Variants} + +\item {\tt replace {\term$_1$} with {\term$_2$} in \ident}\\ + This replaces {\term$_1$} with {\term$_2$} in the hypothesis named + {\ident}, and generates the subgoal {\term$_2$}{\tt =}{\term$_1$}. + + \begin{ErrMsgs} + \item \errindex{No such hypothesis} : {\ident} + \item \errindex{Nothing to rewrite in {\ident}} + \end{ErrMsgs} + +\end{Variants} \subsection{\tt reflexivity \label{reflexivity} -- cgit v1.2.3