diff options
| author | herbelin | 2002-09-09 09:44:51 +0000 |
|---|---|---|
| committer | herbelin | 2002-09-09 09:44:51 +0000 |
| commit | bdca3152f4b0b0ad8e6f2dbb8907cf2391d51603 (patch) | |
| tree | 1636ec8b9963f26ddb6205981e8d29b2841d0f1c /doc | |
| parent | 1cca95b23a15ad0dfa3a79ff07ac57f870c333f0 (diff) | |
MAJ syntaxe 'Hint Rewrite'
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8289 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/RefMan-tac.tex | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/doc/RefMan-tac.tex b/doc/RefMan-tac.tex index 9aacb3fda0..34aa2a2254 100644 --- a/doc/RefMan-tac.tex +++ b/doc/RefMan-tac.tex @@ -1911,28 +1911,28 @@ 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. \end{Variant} -\subsection{\tt HintRewrite [ \term$_1$ \dots \term$_n$ ] in \ident} -\comindex{HintRewrite} +\subsection{\tt Hint Rewrite [ \term$_1$ \dots \term$_n$ ] in \ident} +\comindex{Hint Rewrite} This vernacular command adds the terms {\tt \term$_1$ \dots \term$_n$} (their types must be equalities) in the rewriting base {\tt \ident} with the default orientation (left to right). This command is synchronous with the section mechanism (see \ref{Section}): -when closing a section, all aliases created by \texttt{HintRewrite} in that -section are lost. Conversely, when loading a module, all \texttt{HintRewrite} +when closing a section, all aliases created by \texttt{Hint Rewrite} in that +section are lost. Conversely, when loading a module, all \texttt{Hint Rewrite} declarations at the global level of that module are loaded. \begin{Variants} -\item {\tt HintRewrite -> [ \term$_1$ \dots \term$_n$ ] in \ident}\\ +\item {\tt Hint Rewrite -> [ \term$_1$ \dots \term$_n$ ] in \ident}\\ This is strictly equivalent to the command above (we only precise the orientation which is the default one). -\item {\tt HintRewrite <- [ \term$_1$ \dots \term$_n$ ] in \ident}\\ +\item {\tt Hint Rewrite <- [ \term$_1$ \dots \term$_n$ ] in \ident}\\ Adds the rewriting rules {\tt \term$_1$ \dots \term$_n$} with a right-to-left orientation in the base {\tt \ident}. -\item {\tt HintRewrite [ \term$_1$ \dots \term$_n$ ] in {\ident} using \tac}\\ +\item {\tt Hint Rewrite [ \term$_1$ \dots \term$_n$ ] in {\ident} using \tac}\\ 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. |