Hint Rewrite, ancienne syntaxe

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8500 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 9 insertions, 1 deletions

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