From 1be525103c2c281feaafba4143b69d4d5e4395e6 Mon Sep 17 00:00:00 2001
From: herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Fri, 19 Mar 2004 18:37:47 +0000
Subject: Hint Rewrite, ancienne syntaxe

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

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

diff --git a/doc/RefMan-tac.tex b/doc/RefMan-tac.tex
index 5cb4b1169..aa38ed57a 100644
--- a/doc/RefMan-tac.tex
+++ b/doc/RefMan-tac.tex
@@ -2590,7 +2590,7 @@ $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 syntactic variants for
+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}.
@@ -2624,6 +2624,14 @@ orientation in the base {\tt \ident}.
 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}}.
+
 \end{Variants}
 
 \SeeAlso \ref{autorewrite-example} for examples showing the use of
-- 
cgit v1.2.3

