From 1be525103c2c281feaafba4143b69d4d5e4395e6 Mon Sep 17 00:00:00 2001 From: herbelin 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') 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