From 428c093fd82db3148b021bceb6eb346db91aa60b Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 24 Mar 2004 20:43:23 +0000
Subject: MAJ passage coqart a la nouvelle syntaxe de autorewrite et hint
 rewrite

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

diff --git a/doc/RefMan-tac.tex b/doc/RefMan-tac.tex
index aa38ed57a6..39a98441fb 100644
--- a/doc/RefMan-tac.tex
+++ b/doc/RefMan-tac.tex
@@ -2587,14 +2587,12 @@ command.
 \item {\tt autorewrite with \ident$_1$ \dots \ident$_n$ using \tac}\\
 Performs, in the same way, all the rewritings of the bases {\tt $ident_1$ $...$
 $ident_n$} applying {\tt \tac} to the main subgoal after each rewriting step.
-
-\item{\tt autorewrite [ \ident$_1$ \dots \ident$_n$ ]}\\
-{\tt autorewrite  [ \ident$_1$ \dots \ident$_n$ ] using \tac}\\
-These are deprecated syntactic variants for
-{\tt autorewrite with \ident$_1$ \dots \ident$_n$}
-and
-{\tt autorewrite  with \ident$_1$ \dots \ident$_n$ using \tac}.
-
+%\item{\tt autorewrite [ \ident$_1$ \dots \ident$_n$ ]}\\
+%{\tt autorewrite  [ \ident$_1$ \dots \ident$_n$ ] using \tac}\\
+%These are deprecated syntactic variants for
+%{\tt autorewrite with \ident$_1$ \dots \ident$_n$}
+%and
+%{\tt autorewrite  with \ident$_1$ \dots \ident$_n$ using \tac}.
 \end{Variant}
 
 \subsection{\tt Hint Rewrite \term$_1$ \dots \term$_n$ : \ident
@@ -2625,12 +2623,12 @@ When the rewriting rules {\tt \term$_1$ \dots \term$_n$} in {\tt \ident} will
 be used, the tactic {\tt \tac} will be applied to the generated subgoals, the
 main subgoal excluded.
 
-\item 
-{\tt Hint Rewrite [ \term$_1$ \dots \term$_n$ ] in \ident}\\
-{\tt Hint Rewrite [ \term$_1$ \dots \term$_n$ ] in {\ident} using {\tac}}\\
-These are deprecated syntactic variants for
-{\tt Hint Rewrite \term$_1$ \dots \term$_n$ : \ident} and
-{\tt Hint Rewrite \term$_1$ \dots \term$_n$ using {\tac} : {\ident}}.
+%% \item 
+%% {\tt Hint Rewrite [ \term$_1$ \dots \term$_n$ ] in \ident}\\
+%% {\tt Hint Rewrite [ \term$_1$ \dots \term$_n$ ] in {\ident} using {\tac}}\\
+%% These are deprecated syntactic variants for
+%% {\tt Hint Rewrite \term$_1$ \dots \term$_n$ : \ident} and
+%% {\tt Hint Rewrite \term$_1$ \dots \term$_n$ using {\tac} : {\ident}}.
 
 \end{Variants}
 
-- 
cgit v1.2.3