From 1b7c478d62af9cc9d3da9ab8512d161be5028a13 Mon Sep 17 00:00:00 2001
From: letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Sun, 1 Jun 2008 20:50:57 +0000
Subject: remove additional occurrences of +/- forgotten in commit 11030

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

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

diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index 12b848102..ed1ee75cc 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -2053,7 +2053,7 @@ This happens if \term$_1$ does not occur in the goal.
     and \texttt{rewrite H in * |-} that succeeds if at
     least one of these two tactics succeeds. 
   \end{itemize}
-  Orientation {\tt ->} or {\tt <-} (or {\tt +} or {\tt -}) can be
+  Orientation {\tt ->} or {\tt <-} can be
   inserted before the term to rewrite.
 
 \item {\tt rewrite {\term} at \textit{occurrences}}
@@ -2075,7 +2075,7 @@ This happens if \term$_1$ does not occur in the goal.
   Is equivalent to the $n$ successive tactics {\tt rewrite $\term_1$}
   up to {\tt rewrite $\term_n$}, each one working on the first subgoal
   generated by the previous one.
-  Orientation {\tt ->} or {\tt <-} (or {\tt +} or {\tt -}) can be
+  Orientation {\tt ->} or {\tt <-} can be
   inserted before each term to rewrite. One unique \textit{clause}
   can be added at the end after the keyword {\tt in}, it will 
   then affect all rewrite operations.
-- 
cgit v1.2.3

