diff options
author | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-03-17 19:33:31 +0000 |
---|---|---|
committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-03-17 19:33:31 +0000 |
commit | 31ed89d3a0f0435edfe064bbe26ce810d7f6494f (patch) | |
tree | 5a84aba4947a19316c7e267fadf7b961225887a8 /doc | |
parent | 06a95b6273927a79cd47ac30e84aeed64724554d (diff) |
MAJ autorewrite/Hint Rewrite
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8498 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'doc')
-rw-r--r-- | doc/RefMan-tac.tex | 18 | ||||
-rw-r--r-- | doc/RefMan-tacex.tex | 10 |
2 files changed, 18 insertions, 10 deletions
diff --git a/doc/RefMan-tac.tex b/doc/RefMan-tac.tex index 5c78dcdec..5cb4b1169 100644 --- a/doc/RefMan-tac.tex +++ b/doc/RefMan-tac.tex @@ -1754,7 +1754,7 @@ Analogous to {\tt dependent rewrite ->} but uses the equality from right to left. \end{Variants} -\section{inversion +\section{Inversion \label{inversion}} \subsection{\tt inversion {\ident} @@ -2561,7 +2561,7 @@ intros; fourier. Reset Initial. \end{coq_eval} -\subsection{\tt autorewrite [ \ident$_1$ \dots \ident$_n$ ] +\subsection{\tt autorewrite with \ident$_1$ \dots \ident$_n$. \tacindex{autorewrite}} This tactic \footnote{The behavior of this tactic has much changed compared to @@ -2584,9 +2584,17 @@ command. \Warning{} This tactic may loop if you build non terminating rewriting systems. \begin{Variant} -\item {\tt autorewrite [ \ident$_1$ \dots \ident$_n$ ] using \tac}\\ +\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 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 @@ -2605,8 +2613,8 @@ declarations at the global level of that module are loaded. \begin{Variants} \item {\tt Hint Rewrite -> \term$_1$ \dots \term$_n$ : \ident}\\ -This is strictly equivalent to the command above (we only precise the -orientation which is the default one). +This is strictly equivalent to the command above (we only make explicit the +orientation which otherwise defaults to {\tt ->}). \item {\tt Hint Rewrite <- \term$_1$ \dots \term$_n$ : \ident}\\ Adds the rewriting rules {\tt \term$_1$ \dots \term$_n$} with a right-to-left diff --git a/doc/RefMan-tacex.tex b/doc/RefMan-tacex.tex index 98ae9a7db..ecd54f449 100644 --- a/doc/RefMan-tacex.tex +++ b/doc/RefMan-tacex.tex @@ -594,10 +594,10 @@ Axiom Ack2 : forall n m:nat, Ack (S n) (S m) = Ack n (Ack (S n) m). \end{coq_example*} \begin{coq_example} -Hint Rewrite [ Ack0 Ack1 Ack2 ] in base0. +Hint Rewrite Ack0 Ack1 Ack2 : base0. Lemma ResAck0 : Ack 3 2 = 29. -autorewrite [ base0 ] using try reflexivity. +autorewrite with base0 using try reflexivity. \end{coq_example} \begin{coq_eval} @@ -624,10 +624,10 @@ Axiom \end{coq_example*} \begin{coq_example} -Hint Rewrite [ g0 g1 g2 ] in base1 using omega. +Hint Rewrite g0 g1 g2 using omega : base1. Lemma Resg0 : g 1 110 = 100. -autorewrite [ base1 ] using reflexivity || simpl. +autorewrite with base1 using reflexivity || simpl. \end{coq_example} \begin{coq_eval} @@ -636,7 +636,7 @@ Abort. \begin{coq_example} Lemma Resg1 : g 1 95 = 91. -autorewrite [ base1 ] using reflexivity || simpl. +autorewrite with base1 using reflexivity || simpl. \end{coq_example} \begin{coq_eval} |