From 1aaf8963f655ce8d81ca9e30ddde4334a8cc1987 Mon Sep 17 00:00:00 2001
From: jforest
Date: Mon, 12 Jun 2006 17:00:50 +0000
Subject: Typo in replace doc.

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

(limited to 'doc')

diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index 0c60a4ea73..dce70c6661 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -1555,12 +1555,11 @@ n}| assumption || symmetry; try assumption]}.
 %   \item \errindex{Nothing to rewrite in {\ident}}
 %   \end{ErrMsgs}
 
-\item {\tt replace {\term$_1$} with  {\term$_2$} by \tac} This acts as
+\item {\tt replace {\term$_1$} with  {\term$_2$} by \tac}\\ This acts as
   {\tt  replace {\term$_1$}  with {\term$_2$}}  but try  to  solve the
   generated subgoal {\tt \term$_2$=\term$_1$} using {\tt \tac}.
-\item {\tt replace {\term$_1$} with  {\term$_2$} in \ident by \tac} This acts as
-  {\tt  replace {\term$_1$}  with {\term$_2$} in \ident}  but try  to  solve the
-  generated subgoal {\tt \term$_2$=\term$_1$} using {\tt \tac}.
+\item {\tt replace {\term$_1$} with {\term$_2$} in \ident by \tac}\\
+  This acts as {\tt replace {\term$_1$} with {\term$_2$} in \ident} but try to solve the generated subgoal {\tt \term$_2$=\term$_1$} using {\tt \tac}.
 \end{Variants}
 
 \subsection{\tt reflexivity
-- 
cgit v1.2.3