diff options
| author | herbelin | 2004-03-24 20:43:23 +0000 |
|---|---|---|
| committer | herbelin | 2004-03-24 20:43:23 +0000 |
| commit | 428c093fd82db3148b021bceb6eb346db91aa60b (patch) | |
| tree | ebd07e992b5012469d5fa0c36b0c7a91db6461bb | |
| parent | 0665acd59ee71d20eeec58e2f5c5a27f11ae51e4 (diff) | |
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
| -rw-r--r-- | doc/RefMan-tac.tex | 26 |
1 files 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} |