Revision Tauto, AutoRewrite + Ajout de Ltac

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

5 files changed, 900 insertions, 117 deletions

diff --git a/doc/RefMan-ltac.tex b/doc/RefMan-ltac.tex
index 55d2790d8c..bc79cbbe81 100644
--- a/doc/RefMan-ltac.tex
+++ b/doc/RefMan-ltac.tex
@@ -1,4 +1,785 @@
 \chapter{The tactic language}
 \label{TacticLanguage}
 
-**TO DO**
\ No newline at end of file
+% Très très provisoire
+% À articuler notamment avec le chapitre "Tactiques utilisateurs"
+
+%\geometry{a4paper,body={5in,8in}}
+
+This chapter gives a compact documentation of the tactic language available in
+the toplevel of {\Coq}. We start by giving the syntax and, next, we present the
+informal semantic. Finally, we show some examples which deal with small but
+also with non-trivial problems. If you want to know more regarding this
+language and especially about its fundations, you can refer to~\cite{LTAC}.
+
+\section{Syntax}
+
+The syntax of the tactic language is given in table~\ref{ltac}. We use a
+\bn{}-like notation. Terminal symbols are set in sans serif font ({\sf like
+this}). Non-terminal symbols are set in italic font ($like\sm{}that$). ... {\it
+|} ... denotes the or operation. ...$^*$ denotes zero, one or several
+repetitions. ...$^+$ denotes one or several repetitions. Parentheses {\it
+(}...{\it )} denote grouping. The main entry is $expr$ and the entries $nat$,
+$ident$, $term$ and $primitive\_tactic$ represent respectively the natural
+numbers, the authorized identificators, {\Coq}'s terms and all the basic
+tactics. In $term$, there can be specific variables like {\sf ?n} where {\sf n}
+is a $nat$ or {\sf ?}, which are metavariables for pattern matching. {\sf ?n}
+allows us to keep instantiations and to make constraints whereas {\sf ?} shows
+that we are not interested in what will be matched.
+
+This language is used in proof mode but it can also be used in toplevel
+definitions as shown in table~\ref{ltactop}.
+
+\begin{table}[htbp]
+\noindent{}\framebox[6in][l]
+{\parbox{6in}
+{\begin{center}
+\begin{tabular}{lp{0.1in}l}
+$expr$ & \cn{}::= & $expr$ {\sf ;} $expr$\\
+& \cn{}| & $expr$ {\sf ; [} {\it (}$expr$ {\sf |}{\it )}$^*$ $expr$ {\sf ]}\\
+& \cn{}| & $atom$\\
+\\
+$atom$ & \cn{}::= & {\sf Fun} $input\_fun^+$  {\sf ->} $expr$\\
+& \cn{}| &
+{\sf Let} {\it (}$let\_clause$ {\sf And}{\it )}$^*$ $let\_clause$ {\sf In}
+$expr$\\
+& \cn{}| & {\sf Rec} $rec\_clause$\\
+& \cn{}| &
+{\sf Rec} {\it (}$rec\_clause$ {\sf And}{\it )}$^*$ $rec\_clause$ {\sf In}
+$expr$\\
+& \cn{}| &
+{\sf Match Context With} {\it (}$context\_rule$ {\sf |}{\it )}$^*$
+$context\_rule$\\
+& \cn{}| &
+{\sf Match} $term$ {\sf With} {\it (}$match\_rule$ {\sf |}{\it
+)}$^*$ $match\_rule$\\
+& \cn{}| & {\sf (} $expr$ {\sf )}\\
+& \cn{}| & {\sf (} $expr$ $expr^+$ {\sf )}\\
+& \cn{}| & $atom$ {\sf Orelse} $atom$\\
+& \cn{}| & {\sf Do} {\it (}$int$ {\it |} $ident${\it )} $atom$\\
+& \cn{}| & {\sf Repeat} $atom$\\
+& \cn{}| & {\sf Try} $atom$\\
+& \cn{}| & {\sf First [} {\it (}$expr$ {\sf |}{\it )}$^*$ $expr$ {\sf ]}\\
+& \cn{}| & {\sf Solve [} {\it (}$expr$ {\sf |}{\it )}$^*$ $expr$ {\sf ]}\\
+& \cn{}| & {\sf Idtac}\\
+& \cn{}| & {\sf Fail}\\
+& \cn{}| & $primitive\_tactic$\\
+& \cn{}| & $arg$\\
+\\
+$input\_fun$ & \cn{}::= & $ident$\\
+& \cn{}| & {\sf ()}\\
+\\
+$let\_clause$ & \cn{}::= & $ident$ {\sf =} $expr$\\
+\\
+$rec\_clause$ & \cn{}::= & $ident$ $input\_fun^+$ {\sf ->} $expr$\\
+\\
+$context\_rule$ & \cn{}::= &
+{\sf [} {\it (}$context\_hyps$ {\sf ;}{\it )}$^*$ $context\_hyps$ {\sf |-}
+$term$ {\sf ] ->} $expr$\\
+& \cn{}| & {\sf [ |-} $term$ {\sf ] ->} $expr$\\
+& \cn{}| & {\sf \_ ->} $expr$\\
+\\
+$context\_hyps$ & \cn{}::= & $ident$ {\sf :} $term$\\
+& \cn{}| & {\sf \_ :} $term$\\
+\\
+$match\_rule$ & \cn{}::= & {\sf [} $term$ {\sf ] ->} $expr$\\
+& \cn{}| & {\sf \_ ->} $expr$\\
+\\
+$arg$ & \cn{}::= & {\sf ()}\\
+& \cn{}| & $nat$\\
+& \cn{}| & $ident$\\
+& \cn{}| & {\sf '}$term$
+\end{tabular}
+\end{center}}}
+\caption{Syntax of the tactic language}
+\label{ltac}
+\end{table}
+
+\begin{table}[ht]
+\noindent{}\framebox[6in][l]
+{\parbox{6in}
+{\begin{center}
+\begin{tabular}{lp{0.1in}l}
+$top$ & \cn{}::= & {\sf Tactic Definition} $ident$ $input\_fun^*$ {\sf :=}
+$expr$ \\
+& \cn{}| & {\sf Recursive Tactic Definition} {\it (}$trec\_clause$ {\sf
+And}{\it )}$^*$ $trec\_clause$\\
+\\
+$trec\_clause$ & \cn{}::= & $ident$ $input\_fun^+$ {\sf :=} $expr$
+\end{tabular}
+\end{center}}}
+\caption{Tactic toplevel definitions}
+\label{ltactop}
+\end{table}
+
+\section{Semantic}
+
+\subsection{Values}
+
+Values are given by table~\ref{ltacval}. All these values are tactic values,
+i.e. to be applied to a goal, except {\sf Fun}, {\sf Rec} and $arg$ values.
+
+\begin{table}[ht]
+\noindent{}\framebox[6in][l]
+{\parbox{6in}
+{\begin{center}
+\begin{tabular}{lp{0.1in}l}
+$vexpr$ & \cn{}::= & $vexpr$ {\sf ;} $vexpr$\\
+& \cn{}| & $vexpr$ {\sf ; [} {\it (}$vexpr$ {\sf |}{\it )}$^*$ $vexpr$ {\sf
+]}\\
+& \cn{}| & $vatom$\\
+\\
+$vatom$ & \cn{}::= & {\sf Fun} $input\_fun^+$  {\sf ->} $expr$\\
+& \cn{}| & {\sf Rec} $rec\_clause$\\
+& \cn{}| &
+{\sf Rec} {\it (}$rec\_clause$ {\sf And}{\it )}$^*$ $rec\_clause$ {\sf In}
+$expr$\\
+& \cn{}| &
+{\sf Match Context With} {\it (}$context\_rule$ {\sf |}{\it )}$^*$
+$context\_rule$\\
+& \cn{}| & {\sf (} $vexpr$ {\sf )}\\
+& \cn{}| & $vatom$ {\sf Orelse} $vatom$\\
+& \cn{}| & {\sf Do} {\it (}$int$ {\it |} $ident${\it )} $vatom$\\
+& \cn{}| & {\sf Repeat} $vatom$\\
+& \cn{}| & {\sf Try} $vatom$\\
+& \cn{}| & {\sf First [} {\it (}$vexpr$ {\sf |}{\it )}$^*$ $vexpr$ {\sf ]}\\
+& \cn{}| & {\sf Solve [} {\it (}$vexpr$ {\sf |}{\it )}$^*$ $vexpr$ {\sf ]}\\
+& \cn{}| & {\sf Idtac}\\
+& \cn{}| & {\sf Fail}\\
+& \cn{}| & $primitive\_tactic$\\
+& \cn{}| & $arg$
+\end{tabular}
+\end{center}}}
+\caption{Values of ${\cal L}_{tac}$}
+\label{ltacval}
+\end{table}
+
+\subsection{Evaluation}
+
+\subsubsection{Local definitions}
+
+Local definitions can be done as follows:
+
+\newpage{}
+
+\phantom{}
+\vfill{}
+
+\begin{tabbing}
+{\sf And} \=\kill
+{\sf Let}\>$ident_1$ {\sf =} $expr_1$\\
+{\sf And} $ident_2$ {\sf =} $expr_2$\\
+...\\
+{\sf And} $ident_n$ {\sf =} $expr_n$ {\sf In}\\
+\>$expr$
+\end{tabbing}
+
+$expr_i$ is evaluated to $v_i$, then, $expr$ is evaluated by subsituting $v_i$
+to each occurrence of $ident_i$, for $i=1,...,n$. There is no dependencies
+between the $expr_i$ and the $ident_i$.
+
+\subsubsection{Pattern matching on terms}
+
+We can carry out pattern matching on terms with:
+
+\newpage{}
+
+\begin{tabbing}
+\hx{3}\={\sf |} \=$term_n$ \=\kill
+{\sf Match} $term$ {\sf With}\\
+\>\>$term_1$ {\sf ->} $expr_1$\\
+\>{\sf |} $term_2$ {\sf ->} $expr_2$\\
+\>...\\
+\>{\sf |} $term_n$ {\sf ->} $expr_n$\\
+\>{\sf |} {\sf \_}\>\>{\sf ->} $expr_{n+1}$
+\end{tabbing}
+
+if $term$ is matched (non-linear first order unification) by $term_1$ then
+$expr_1$ is evaluated by substituting the pattern matching instantiations to
+the metavariables. Else, $term_2$ is tried and so on. If no $term_i$, with
+$i=1,...,n$, matches $term$ then the last clause is used and $expr_{n+1}$ is
+evaluated.\\
+
+{\sf Error message:}\\
+
+{\tt No matching clauses for Match}
+
+\hx{4}No pattern can be used and, in particular, there is no {\sf \_} pattern.
+
+\subsubsection{Application}
+
+An application is an expression of the following form:\\
+
+{\sf (} $expr$ $expr_1$ ... $expr_n$ {\sf )}\\
+
+$expr$ is evaluated to $v$ and $expr_i$ is evaluated to $v_i$, for $i=1,...,n$.
+If $expr$ is a {\sf Fun} or {\sf Rec} value then the body is evaluated by
+substituting $v_i$ to the formal parameters, for $i=1,...,n$. For recursive
+clauses, the bodies are lazily substituted (when an identifier to be evaluated
+is the name of a recursive clause).
+
+\subsection{Application of tactic values}
+
+\subsubsection{Sequence}
+
+A sequence is an expression of the following form:\\
+
+$expr_1$ {\sf ;} $expr_2$\\
+
+$expr_1$ and $expr_2$ are evaluated to $v_1$ and $v_2$. $v_1$ and $v_2$ must be
+tactic values. $v_1$ is then applied and $v_2$ is applied to the subgoals
+generated by the application of $v_1$. Sequence is left associating.
+
+\subsubsection{General sequence}
+
+We can generalize the previous sequence operator by:\\
+
+$expr_0$ {\sf ; [} $expr_1$ {\sf |} $...$ {\sf |} $expr_n$ {\sf ]}\\
+
+$expr_i$ is evaluated to $v_i$, for $i=0,...,n$. $v_0$ is applied and $v_i$ is
+applied to the $i$-th generated subgoal by the application of $v_0$, for
+$=1,...,n$. It fails if the application of $v_0$ does not generate exactly $n$
+subgoals.
+
+\subsubsection{Branching}
+
+We can easily branch with the following structure:\\
+
+$expr_1$ {\sf Orelse} $expr_2$\\
+
+$expr_1$ and $expr_2$ are evaluated to $v_1$ and $v_2$. $v_1$ and $v_2$ must be
+tactic values. $v_1$ is applied and if it fails then $v_2$ is applied.
+Branching is left associating.
+
+\subsubsection{For loop}
+
+We have a for loop with:\\
+
+{\sf Do} $n$ $expr$\\
+
+$expr$ is evaluated to $v$. $v$ must be a tactic value. $v$ is applied $n$
+times. Supposing $n>1$, after the first application of $v$, $v$ is applied, at
+least once, to the generated subgoals and so on. It fails if the application of
+$v$ fails before the $n$ applications have been completed.
+
+\subsubsection{Repeat loop}
+
+We have a repeat loop with:\\
+
+{\sf Repeat} $expr$\\
+
+$expr$ is evaluated to $v$. $v$ must be a tactic value. $v$ is applied until it
+fails. Supposing $n>1$, after the first application of $v$, $v$ is applied, at
+least once, to the generated subgoals and so on. It stops when it fails for all
+the generated subgoals. It never fails.
+
+\subsubsection{Error catching}
+
+We can catch the tactic errors with:\\
+
+{\sf Try} $expr$\\
+
+$expr$ is evaluated to $v$. $v$ must be a tactic value. $v$ is applied. If the
+application of $v$ fails, it catches the error and leaves the goal unchanged.
+It never fails.
+
+\subsubsection{First tactic to work}
+
+We may consider the first tactic to work (i.e. which does not fail) among a
+panel of tactics:\\
+
+{\sf First [} $expr_1$ {\sf |} $...$ {\sf |} $expr_n$ {\sf ]}\\
+
+$expr_i$ are evaluated to $v_i$ and $v_i$ must be tactic values, for 
+$i=1,...,n$. Supposing $n>1$, it applies $v_1$, if it works, it stops else it
+tries to apply $v_2$ and so on. It fails when there is no applicable tactic.\\
+
+{\sf Error message:}\\
+
+{\tt No applicable tactic}
+
+\subsubsection{Solving}
+
+We may consider the first to solve (i.e. which generates no subgoal) among a
+panel of tactics:\\
+
+{\sf Solve [} $expr_1$ {\sf |} $...$ {\sf |} $expr_n$ {\sf ]}\\
+
+$expr_i$ are evaluated to $v_i$ and $v_i$ must be tactic values, for 
+$i=1,...,n$. Supposing $n>1$, it applies $v_1$, if it solves, it stops else it
+tries to apply $v_2$ and so on. It fails if there is no solving tactic.\\
+
+{\sf Error message:}\\
+
+{\tt Cannot solve the goal}
+
+\subsubsection{Identity}
+
+We have the identity tactic:\\
+
+{\sf Idtac}\\
+
+It leaves the goal unchanged but it appears in the proof script.
+
+\subsubsection{Failing}
+
+We have the failing tactic:\\
+
+{\sf Fail}\\
+
+It always fails and leaves the goal unchanged. It does not appear in the proof
+script and can be catched by {\sf Try}.
+
+\subsubsection{Pattern matching on proof contexts}
+
+We can make pattern matching on proof contexts using the following
+expression:
+
+\begin{tabbing}
+\hx{3}\={\sf |}\={\sf [}$context\_hyps_{n,1}${\sf ;}...{\sf ;}$context\_hyps_{n,m_n}$\={\sf |-}$term_n${\sf ] }\=\kill
+{\sf Match Context With}\\
+\>\>{\sf [}$context\_hyps_{1,1}${\sf ;}...{\sf ;}$context\_hyps_{1,m_1}$\>{\sf
+|-}$term_1${\sf ] ->} $expr_1$\\
+\>{\sf |[}$context\_hyps_{2,1}${\sf ;}...{\sf ;}$context\_hyps_{2,m_2}$\>\>{\sf
+|-}$term_2${\sf ] ->} $expr_2$\\
+\>...\\
+\>{\sf |[}$context\_hyps_{n,1}${\sf ;}...{\sf ;}$context\_hyps_{n,m_n}$\>\>{\sf
+|-}$term_n${\sf ] ->} $expr_n$\\
+\>{\sf |\_}\>\>\>{\sf ->} $expr_{n+1}$
+\end{tabbing}
+
+If each hypothesis pattern $context\_hyps_{1,i}$, with $i=1,...,m_1$ is matched
+(non-linear first order unification) by an hypothesis of the goal and if
+$term_1$ is matched by the conclusion of the goal, then $expr_1$ is evaluated
+to $v_1$ by substituting the pattern matching to the metavariables and the real
+hypothesis names bound to the possible hypothesis names occurring in the
+hypothesis patterns. If $v_1$ is a tactic value, then it is applied to the
+goal. If this application fails, then another combination of hypotheses is
+tried with the same proof context pattern. If there is no other combination of
+hypotheses then the second proof context pattern is tried and so on. If the
+next to last proof context pattern fails then $expr_{n+1}$ is evaluated to
+$v_{n+1}$ and $v_{n+1}$ is applied.\\
+
+{\sf Error message:}\\
+
+{\tt No matching clauses for Match Context}
+
+\hx{4}No proof context pattern can be used and, in particular, there is no {\sf
+\_} proof
+
+\hx{4}context pattern.
+
+\subsection{Tactic toplevel definitions}
+
+Basically, tactics toplevel definitions are made as follows:\\
+
+{\sf Tactic Definition} $ident$ {\sf :=} $expr$\\
+
+$expr$ is evaluated to $v$ and $v$ is associated to $ident$. Next, every
+script is evaluated by substituting $v$ to $ident$.
+
+We can define functional definitions by:\\
+
+{\sf Tactic Definition} $ident$ $input\_fun_1$ ... $input\_fun_n$ {\sf :=}
+$expr$\\
+
+This definition is nothing else than syntactical sugar for:\\
+
+{\sf Tactic Definition} $ident$ {\sf := Fun} $input\_fun_1$ ... $input\_fun_n$
+{\sf ->} $expr$\\
+
+Then, this definition is treated as above.
+
+Finally, mutal recursive function definitions are possible with:
+
+\begin{tabbing}
+\hx{4}\={\sf And} \=$ident_n$ $input\_fun_{n,1}$ ... $input\_fun_{n,m_n}$ \=\kill
+\>{\sf Recursive Tactic Definition}\\
+\>\>$ident_1$ $input\_fun_{1,1}$ ...
+$input\_fun_{1,m_1}$\>{\sf :=} $expr_1$\\
+\>{\sf And} $ident_2$ $input\_fun_{2,1}$ ... $input\_fun_{2,m_2}$\>\>{\sf :=}
+$expr_2$\\
+\>...\\
+\>{\sf And} $ident_n$ $input\_fun_{n,1}$ ... $input\_fun_{n,m_n}$ {\sf :=}
+$expr_n$
+\end{tabbing}
+
+This definition bloc is a set of simultaneous functional definitions (use of
+the same previous syntactical sugar) and the other scripts are evaluated as
+usual except that the substitutions are lazily carried out (when an identifier
+to be evaluated is the name of a recursive definition).
+
+\section{Examples}
+
+\subsection{About the cardinality of the natural number set}
+
+A first example which shows how to use the pattern matching over the proof
+contexts is the proof that natural numbers have more than two elements. The
+proof of such a lemma can be done as shown in table~\ref{cnatltac}.
+
+\begin{table}[ht]
+\noindent{}\framebox[6in][l]
+{\parbox{6in}
+{\begin{tabbing}
+\hx{4}\=\hx{4}\=\hx{4}\=\hx{4}\=\hx{4}\=\kill
+\>{\sf Lemma card\_nat: \~{}(EX x:nat|(EX y:nat|(z:nat)(x=z)$\bs{}$/(y=z))).}\\
+\>{\sf Proof.}\\
+\>\>{\sf Red;Intro H.}\\
+\>\>{\sf Elim H;Intros a Ha.}\\
+\>\>{\sf Elim Ha;Intros b Hb.}\\
+\>\>{\sf Elim (Hb (0));Elim (Hb (1));Elim (Hb (2));Intros;}\\
+\>\>\>{\sf Match Context With}\\
+\>\>\>\>{\sf [\_:?1=?2;\_:?1=?3|-?] ->}\\
+\>\>\>\>\>{\sf Cut ?2=?3;[Discriminate|Apply trans\_equal with ?1;Auto].}\\
+\>{\sf Save.}
+\end{tabbing}}}
+\caption{A proof on cardinality of natural numbers}
+\label{cnatltac}
+\end{table}
+
+We can notice that all the (very similar) cases coming from the three
+eliminations (with three distinct natural numbers) are successfully solved by
+a {\sf Match Context} structure and, in particular, with only one pattern (use
+of non-linear unification).
+
+\subsection{Permutation on closed lists}
+
+Another more complex example is the problem of permutation on closed lists. The
+aim is to show that a closed list is a permutation of another one.
+
+First, we define the permutation predicate as shown in table~\ref{permutpred}.
+
+\begin{table}[ht]
+\noindent{}\framebox[6in][l]
+{\parbox{6in}
+{\begin{tabbing}
+\hx{4}\=\hx{4}\={\sf |}\=\hx{3}\=\kill
+\>{\sf Section Sort.}\\
+\\
+\>{\sf Variable A:Set.}\\
+\\
+\>{\sf Inductive permut:(list A)->(list A)->Prop:=}\\
+\>\>\>{\sf  permut\_refl:(l:(list A))(permut l l)}\\
+\>\>{\sf |permut\_cons:}\\
+\>\>\>\>{\sf (a:A)(l0,l1:(list A))(permut l0 l1)->(permut (cons a l0) (cons a
+l1))}\\
+\>\>{\sf |permut\_append:(a:A)(l:(list A))(permut (cons a l) (l\^{}(cons a (nil
+A))))}\\
+\>\>{\sf |permut\_trans:}\\
+\>\>\>\>{\sf (l0,l1,l2:(list A))(permut l0 l1)->(permut l1 l2)->(permut l0
+l2).}\\
+\\
+\>{\sf End Sort.}
+\end{tabbing}}}
+\caption{Definition of the permutation predicate}
+\label{permutpred}
+\end{table}
+
+Next, we can write naturally the tactic and the result can be seen in
+table~\ref{permutltac}. We can notice that we use two toplevel definitions {\sf
+PermutProve} and {\sf Permut}. The function to be called is {\sf PermutProve}
+which computes the lengths of the two lists and calls {\sf Permut} with the
+length if the two lists have the same length. {\sf Permut} works as expected.
+If the two lists are equal, it concludes. Otherwise, if the lists have
+identical first elements, it applies {\sf Permut} on the tail of the lists.
+Finally, if the lists have different first elements, it puts the first element
+of one of the lists (here the second one which appears in the {\sf permut}
+predicate) at the end if that is possible, i.e., if the new first element has
+been at this place previously. To verify that all rotations have been done for
+a list, we use the length of the list as an argument for {\sf Permut} and this
+length is decremented for each rotation down to, but not including, 1 because
+for a list of length $n$, we can make exactly $n-1$ rotations to generate at
+most $n$ distinct lists. Here, it must be noticed that we use the natural
+numbers of {\Coq} for the rotation counter. In table~\ref{ltac}, we can see
+that it is possible to use usual natural numbers but they are only used as
+arguments for primitive tactics and they cannot be handled, in particular, we
+cannot make computations with them. So, a natural choice is to use {\Coq} data
+structures so that {\Coq} makes the computations (reductions) by {\sf Eval
+Compute in} and we can get the terms back by {\sf Match}.
+ 
+\begin{table}[p]
+\noindent{}\framebox[6in][l]
+{\parbox{6in}
+{\begin{tabbing}
+\hx{4}\=\hx{4}\=\hx{4}\={\sf |}\=\hx{3}\=\hx{4}\={\sf |}\=\hx{3}\=\hx{4}\=
+\hx{4}\=\kill
+\>{\sf Tactic Definition Permut n:=}\\
+\>\>{\sf Match Context With}\\
+\>\>\>\>{\sf [|-(permut ? ?1 ?1)] -> Apply permut\_refl}\\
+\>\>\>{\sf |[|-(permut ? (cons ?1 ?2) (cons ?1 ?3))] ->}\\
+\>\>\>\>\>{\sf Let newn=Eval Compute in (length ?2)}\\
+\>\>\>\>\>{\sf In}\\
+\>\>\>\>\>\>{\sf Apply permut\_cons;(Permut newn)}\\
+\>\>\>{\sf |[|-(permut ?1 (cons ?2 ?3) ?4)] ->}\\
+\>\>\>\>\>{\sf (Match Eval Compute in n With}\\
+\>\>\>\>\>\>\>{\sf [(1)] -> Fail}\\
+\>\>\>\>\>\>{\sf |\_ ->}\\
+\>\>\>\>\>\>\>\>{\sf Let l0'='(?3\^{}(cons ?2 (nil ?1)))}\\
+\>\>\>\>\>\>\>\>{\sf In}\\
+\>\>\>\>\>\>\>\>\>{\sf Apply (permut\_trans ?1 (cons ?2 ?3) l0' ?4);}\\
+\>\>\>\>\>\>\>\>\>\>{\sf [Apply permut\_append|}\\
+\>\>\>\>\>\>\>\>\>\>{\sf Compute;(Permut (pred n))]).}\\
+\\
+\>{\sf Tactic Definition PermutProve:=}\\
+\>\>{\sf Match Context With}\\
+\>\>\>\>{\sf [|-(permut ? ?1 ?2)] ->}\\
+\>\>\>\>\>{\sf (Match Eval Compute in ((length ?1)=(length ?2)) With}\\
+\>\>\>\>\>\>\>{\sf [?1=?1] -> (Permut ?1)).}
+\end{tabbing}}}
+\caption{Permutation tactic}
+\label{permutltac}
+\end{table}
+
+With {\sf PermutProve}, we can now prove lemmas such those shown in
+table~\ref{permutlem}.
+
+\begin{table}[p]
+\noindent{}\framebox[6in][l]
+{\parbox{6in}
+{\begin{tabbing}
+\hx{4}\=\hx{4}\=\hx{4}\=\hx{4}\=\kill
+\>{\sf Lemma permut\_ex1:}\\
+\>\>{\sf (permut nat (cons (1) (cons (2) (cons (3) (nil nat))))}\\
+\>\>\>{\sf (cons (3) (cons (2) (cons (1) (nil nat))))).}\\
+\>{\sf Proof.}\\
+\>\>{\sf PermutProve.}\\
+\>{\sf Save.}\\
+\\
+\>{\sf Lemma permut\_ex2:}\\
+\>\>{\sf (permut nat}\\
+\>\>\>{\sf (cons (0) (cons (1) (cons (2) (cons (3) (cons (4) (cons (5) (cons (6)}\\
+\>\>\>\>{\sf (cons (7) (cons (8) (cons (9) (nil nat)))))))))))}\\
+\>\>\>{\sf (cons (0) (cons (2) (cons (4) (cons (6) (cons (8) (cons (9) (cons (7)}\\
+\>\>\>\>{\sf (cons (5) (cons (3) (cons (1) (nil nat)))))))))))).}\\
+\>{\sf Proof.}\\
+\>\>{\sf PermutProve.}\\
+\>{\sf Save.}
+\end{tabbing}}}
+\caption{Examples of {\sf PermutProve} use}
+\label{permutlem}
+\end{table}
+
+\subsection{Deciding intuitionnistic propositional logic}
+
+The pattern matching on proof contexts allows a complete and so a powerful
+backtracking when returning tactic values. An interesting application is the
+problem of deciding intuitionnistic propositional logic. Considering the
+contraction-free sequent calculi {\sf LJT*} of Roy~Dyckhoff (\cite{Dyc92}), it
+is quite natural to code such a tactic using the tactic language as shown in
+table~\ref{tautoltac}. The tactic {\sf Axioms} tries to conclude using usual
+axioms. The tactic {\sf Simplif} applies all the reversible rules of Dyckhoff's
+system. Finally, the tactic {\sf TautoProp} (the main tactic to be called)
+simplifies with {\sf Simplif}, tries to conclude with {\sf Axioms} and tries
+several paths using the backtracking rules (one of the four Dyckhoff's rules
+for the left implication to get rid of the contraction and the right or).
+
+\begin{table}[ht]
+\noindent{}\framebox[6in][l]
+{\parbox{6in}
+{\begin{tabbing}
+\hx{4}\=\hx{4}\=\hx{4}\={\sf |}\=\hx{3}\={\sf |}\=\hx{3}\={\sf |}\=\hx{3}\=\hx{4}\=\hx{4}\=\kill
+\>{\sf Tactic Definition Axioms:=}\\
+\>\>{\sf Match Context With}\\
+\>\>\>\>{\sf [|-True] -> Trivial}\\
+\>\>\>{\sf |[\_:False|- ?] -> ElimType False;Assumption}\\
+\>\>\>{\sf |[\_:?1|-?1] -> Auto.}\\
+\\
+\>{\sf Tactic Definition Simplif:=}\\
+\>\>{\sf Repeat}\\
+\>\>\>{\sf (Intros;}\\
+\>\>\>\>\>{\sf (Match Context With}\\
+\>\>\>\>\>\>\>\>{\sf [id:\~{}?|-?] -> Red in id}\\
+\>\>\>\>\>\>\>{\sf |[id:?/$\bs{}$?|-?] -> Elim id;Do 2 Intro;Clear id}\\
+\>\>\>\>\>\>\>{\sf |[id:?$\bs{}$/?|-?] -> Elim id;Intro;Clear id}\\
+\>\>\>\>\>\>\>{\sf |[id:?1/$\bs{}$?2->?3|-?] ->}\\
+\>\>\>\>\>\>\>\>\>{\sf Cut ?1->?2->?3;[Intro|Intros;Apply id;Split;Assumption]}\\
+\>\>\>\>\>\>\>{\sf |[id:?1$\bs{}$/?2->?3|-?] ->}\\
+\>\>\>\>\>\>\>\>\>{\sf Cut ?2->?3;[Cut ?1->?3;[Intros|}\\
+\>\>\>\>\>\>\>\>\>\>{\sf Intro;Apply id;Left;Assumption]|}\\
+\>\>\>\>\>\>\>\>\>\>{\sf Intro;Apply id;Right;Assumption]}\\
+\>\>\>\>\>\>\>{\sf |[id0:?1->?2;id1:?1|-?] ->}\\
+\>\>\>\>\>\>\>\>\>{\sf Cut ?2;[Intro;Clear id0|Apply id0;Assumption]}\\
+\>\>\>\>\>\>\>{\sf |[|-?/$\bs{}$?] -> Split}\\
+\>\>\>\>\>\>\>{\sf |[|-\~{}?] -> Red)).}\\
+\\
+\>{\sf Recursive Tactic Definition TautoProp:=}\\
+\>\>{\sf Simplif;}\\
+\>\>{\sf Axioms}\\
+\>\>{\sf Orelse}\\
+\>\>\>{\sf Match Context With}\\
+\>\>\>\>\>\>{\sf [id:(?1->?2)->?3|-?] ->}\\
+\>\>\>\>\>\>\>{\sf Cut ?2->?3;[Intro;Cut ?1->?2;[Intro;Cut ?3;[Intro;Clear id|}\\
+\>\>\>\>\>\>\>\>\>{\sf Apply id;Assumption]|Clear id]|}\\
+\>\>\>\>\>\>\>\>\>{\sf Intro;Apply id;Intro;Assumption];TautoProp}\\
+\>\>\>\>\>{\sf |[id:\~{}?1->?2|-?]->}\\
+\>\>\>\>\>\>\>{\sf Cut False->?2;[Intro;Cut ?1->False;[Intro;Cut ?2;[Intro;Clear id|}\\
+\>\>\>\>\>\>\>\>\>{\sf Apply id;Assumption]|Clear id]|}\\
+\>\>\>\>\>\>\>\>\>{\sf Intro;Apply id;Red;Intro;Assumption];TautoProp}\\
+\>\>\>\>\>{\sf |[|-?$\bs{}$/?] ->}\\
+\>\>\>\>\>\>\>{\sf (Left;TautoProp) Orelse (Right;TautoProp).}
+\end{tabbing}}}
+\caption{Deciding intuitionnistic propositions}
+\label{tautoltac}
+\end{table}
+
+For example, with {\sf TautoProp}, we can prove tautologies like those in
+table~\ref{tautolem}.
+
+\begin{table}[ht]
+\noindent{}\framebox[6in][l]
+{\parbox{6in}
+{\begin{tabbing}
+\hx{4}\=\hx{4}\=\hx{4}\=\hx{4}\=\kill
+\>{\sf Lemma tauto\_ex1:(A,B:Prop)A/$\bs{}$B->A$\bs{}$/B.}\\
+\>{\sf Proof.}\\
+\>\>{\sf TautoProp.}\\
+\>{\sf Save.}\\
+\\
+\>{\sf Lemma tauto\_ex2:(A,B:Prop)(\~{}\~{}B->B)->(A->B)->\~{}\~{}A->B.}\\
+\>{\sf Proof.}\\
+\>\>{\sf TautoProp.}\\
+\>{\sf Save.}
+\end{tabbing}}}
+\caption{Proofs of tautologies with {\sf TautoProp}}
+\label{tautolem}
+\end{table}
+
+\subsection{Deciding type isomorphisms}
+
+A more tricky problem is to decide equalities between types and modulo
+isomorphisms. Here, we choose to use the isomorphisms of the simply typed
+$\lb{}$-calculus with Cartesian product and $unit$ type (see, for example,
+\cite{RC95}). The axioms of this $\lb{}$-calculus are given by
+table~\ref{isosax}.
+
+\begin{table}[ht]
+\noindent{}\framebox[6in][l]
+{\parbox{6in}
+{\begin{tabbing}
+\hx{4}\=\hx{4}\=\kill
+\>{\sf Section Iso\_axioms.}\\
+\\
+\>{\sf Variable A,B,C:Set.}\\
+\\
+\>{\sf Axiom Com:(A*B)==(B*A).}\\
+\>{\sf Axiom Ass:(A*(B*C))==((A*B)*C).}\\
+\>{\sf Axiom Cur:((A*B)->C)==(A->B->C).}\\
+\>{\sf Axiom Dis:(A->(B*C))==((A->B)*(A->C)).}\\
+\>{\sf Axiom P\_unit:(A*unit)==A.}\\
+\>{\sf Axiom AR\_unit:(A->unit)==unit.}\\
+\>{\sf Axiom AL\_unit:(unit->A)==A.}\\
+\\
+\>{\sf Lemma Cons:B==C->(A*B)==(A*C).}\\
+\>{\sf Proof.}\\
+\>\>{\sf Intro Heq;Rewrite Heq;Apply refl\_eqT.}\\
+\>{\sf Save.}\\
+\\
+\>{\sf End Iso\_axioms.}
+\end{tabbing}}}
+\caption{Type isomorphism axioms}
+\label{isosax}
+\end{table}
+
+The tactic to judge equalities modulo this axiomatization can be written as
+shown in tables~\ref{isosltac1} and~\ref{isosltac2}. The algorithm is quite
+simple. Types are reduced using axioms that can be oriented (this done by {\sf
+MainSimplif}). The normal forms are sequences of Cartesian
+products without Cartesian product in the left component. These normal forms
+are then compared modulo permutation of the components (this is done by {\sf
+Compare}). The main tactic to be called and realizing this algorithm is
+{\sf IsoProve}.
+
+\begin{table}[ht]
+\noindent{}\framebox[6in][l]
+{\parbox{6in}
+{\begin{tabbing}
+\hx{4}\=\hx{4}\=\hx{4}\={\sf |}\=\hx{3}\=\hx{4}\=\kill
+\>{\sf Recursive Tactic Definition Simplif trm:=}\\
+\>\>{\sf Match trm With}\\
+\>\>\>\>{\sf [(?1*?2)*?3] -> Rewrite <- (Ass ?1 ?2 ?3);Try MainSimplif}\\
+\>\>\>{\sf |[(?1*?2)->?3] -> Rewrite (Cur ?1 ?2 ?3);Try MainSimplif}\\
+\>\>\>{\sf |[?1->(?2*?3)] -> Rewrite (Dis ?1 ?2 ?3);Try MainSimplif}\\
+\>\>\>{\sf |[?1*unit] -> Rewrite (P\_unit ?1);Try MainSimplif}\\
+\>\>\>{\sf |[unit*?1] -> Rewrite (Com unit ?1);Try MainSimplif}\\
+\>\>\>{\sf |[?1->unit] -> Rewrite (AR\_unit ?1);Try MainSimplif}\\
+\>\>\>{\sf |[unit-> ?1] -> Rewrite (AL\_unit ?1);Try MainSimplif}\\
+\>\>\>{\sf |[?1*?2] ->}\\
+\>\>\>\>\>{\sf ((Simplif ?1);Try MainSimplif) Orelse}\\
+\>\>\>\>\>\>{\sf ((Simplif ?2);Try MainSimplif)}\\
+\>\>\>{\sf |[?1-> ?2] ->}\\
+\>\>\>\>\>{\sf ((Simplif ?1);Try MainSimplif) Orelse}\\
+\>\>\>\>\>\>{\sf ((Simplif ?2);Try MainSimplif)}\\
+\>{\sf And MainSimplif:=}\\
+\>\>{\sf Match Context With}\\
+\>\>\>\>{\sf [|- ?1== ?2] -> Try (Simplif ?1);Try (Simplif ?2).}\\
+\\
+\>{\sf Tactic Definition Length trm:=}\\
+\>\>{\sf Match trm With}\\
+\>\>\>\>{\sf [?*?1] ->}\\
+\>\>\>\>\>{\sf Let succ=(Length ?1)}\\
+\>\>\>\>\>{\sf In}\\
+\>\>\>\>\>\>{\sf '(S succ)}\\
+\>\>\>{\sf |\_ -> '(1).}\\
+\\
+\>{\sf Tactic Definition Assoc:= Repeat Rewrite <- Ass.}
+\end{tabbing}}}
+\caption{Type isomorphism tactic (1)}
+\label{isosltac1}
+\end{table}
+
+\begin{table}[ht]
+\noindent{}\framebox[6in][l]
+{\parbox{6in}
+{\begin{tabbing}
+\hx{4}\=\hx{4}\=\hx{4}\={\sf |}\=\hx{3}\=\hx{4}\={\sf |}\=\hx{3}\=\hx{1}\=\hx{3}\=\kill
+\>{\sf Recursive Tactic Definition DoCompare n:=}\\
+\>\>{\sf Match Context With}\\
+\>\>\>\>{\sf [|-?1==?1] -> Apply refl\_eqT}\\
+\>\>\>{\sf |[|-(?1*?2)==(?1*?3)] ->}\\
+\>\>\>\>\>{\sf Apply Cons;}\\
+\>\>\>\>\>\>{\sf Let newn=(Length ?2)}\\
+\>\>\>\>\>\>{\sf  In}\\
+\>\>\>\>\>\>\>\>{\sf (DoCompare newn)}\\
+\>\>\>{\sf |[|-(?1*?2)==?3] ->}\\
+\>\>\>\>\>{\sf (Match Eval Compute in n With}\\
+\>\>\>\>\>\>\>{\sf [(1)] -> Fail}\\
+\>\>\>\>\>\>{\sf |\_ -> }\\
+\>\>\>\>\>\>\>\>{\sf Pattern 1 (?1*?2);Rewrite Com;Assoc;}\\
+\>\>\>\>\>\>\>\>\>\>{\sf (DoCompare '(pred n))).}\\
+\\
+\>{\sf Tactic Definition Compare:=}\\
+\>\>{\sf Match Context With}\\
+\>\>\>\>{\sf [|-?1==?2] ->}\\
+\>\>\>\>\>{\sf Let l1=(Length ?1)}\\
+\>\>\>\>\>{\sf And l2=(Length ?2)}\\
+\>\>\>\>\>{\sf In}\\
+\>\>\>\>\>\>{\sf (Match Eval Compute in l1=l2 With}\\
+\>\>\>\>\>\>\>\>\>{\sf [?1=?1] -> (DoCompare ?1)).}\\
+\\
+\>{\sf Tactic Definition IsoProve:=MainSimplif;Compare.}
+\end{tabbing}}}
+\caption{Type isomorphism tactic (2)}
+\label{isosltac2}
+\end{table}
+
+Table~\ref{isoslem} gives examples of what can be solved by {\sf IsoProve}.
+
+\begin{table}[ht]
+\noindent{}\framebox[6in][l]
+{\parbox{6in}
+{\begin{tabbing}
+\hx{4}\=\hx{4}\=\kill
+\>{\sf Lemma isos\_ex1:(A,B:Set)((A*unit)*B)==(B*(unit*A)).}\\
+\>{\sf Proof.}\\
+\>\>{\sf Intros;IsoProve.}\\
+\>{\sf Save.}\\
+\\
+\>{\sf Lemma isos\_ex2:(A,B,C:Set)}\\
+\>\>{\sf ((A*unit)->(B*C*unit))==(((A*unit)->((C->unit)*C))*(unit->(A->B))).}\\
+\>{\sf Proof.}\\
+\>\>{\sf Intros;IsoProve.}\\
+\>{\sf Save.}
+\end{tabbing}}}
+\caption{Type equalities solved by {\sf IsoProve}}
+\label{isoslem}
+\end{table}
diff --git a/doc/RefMan-tac.tex b/doc/RefMan-tac.tex
index adc76dffef..5f82ef8f69 100644
--- a/doc/RefMan-tac.tex
+++ b/doc/RefMan-tac.tex
@@ -1461,15 +1461,19 @@ depth is {\tt \num}.
   The Prolog tactic was not able to prove the subgoal.
 \end{ErrMsgs}
 
-\subsection{\tt Tauto}\tacindex{Tauto}\label{Tauto}
-This tactic, due to César Mu\~noz \cite{Mun94}, implements a
-decision procedure for intuitionistic propositional calculus based on
-the contraction-free sequent calculi LJT* of R. Dyckhoff \cite{Dyc92}.
-Note tha
- t {\tt Tauto} succeeds on any instance of an intuitionistic
-tautological proposition. For instance it succeeds on
-\verb!(x:nat)(P:nat->Prop)x=O\/(P x)->~x=O->(P x)!
-while {\tt Auto} fails.
+\subsection{\tt Tauto}
+\tacindex{Tauto}\label{Tauto}
+
+This tactic implements a decision procedure for intuitionistic propositional
+calculus based on the contraction-free sequent calculi LJT* of Roy Dyckhoff
+\cite{Dyc92}. Note that {\tt Tauto} succeeds on any instance of an
+intuitionistic tautological proposition. For instance, it succeeds on:
+
+\begin{verbatim}
+(x:nat)(P:nat->Prop)x=O\/(P x)->~x=O->(P x)
+\end{verbatim}
+
+\noindent{}while {\tt Auto} fails.
 
 \subsection{\tt Intuition}
 \tacindex{Intuition}\label{Intuition}
@@ -1491,6 +1495,14 @@ internally replaces it by the equivalent one:
 \end{verbatim}
 and then uses {\tt Auto with *} which completes the proof.
 
+Originally due to César~Muñoz, these tactics ({\tt Tauto} and {\tt Intuition})
+have been completely reenginered by David~Delahaye using mainly the tactic
+language (see chapter~\ref{TacticLanguage}). The code is now quite shorter and
+a significant increase in performances has been noticed. The general behavior
+with respect to dependent types has slightly changed to get clearer semantics.
+This may lead to some incompatibilities.
+
+\SeeAlso file \texttt{contrib/Rocq/DEMOS/Demo\_tauto.v}
 
 % \subsection{\tt Linear}\tacindex{Linear}\label{Linear}
 % The tactic \texttt{Linear}, due to Jean-Christophe Filliâatre
@@ -1611,88 +1623,64 @@ You can have a look at the files \texttt{Ring.v},
 
 \SeeAlso Chapter~\ref{Ring} for more detailed explanations about this tactic.
 
-\subsection{\tt AutoRewrite [{\rewrule} {\dots} {\rewrule}]}
+\subsection{\tt AutoRewrite  [ \ident$_1$ \dots \ident$_n$ ]}
 \tacindex{AutoRewrite}
 
-This tactic carries out rewritings according the given rewriting
-rules.
+This tactic \footnote{The behavior of this tactic has much changed compared to
+the versions available in the previous distributions (V6). This may cause
+significant changes in your theories to obtain the same result. As a drawback
+of the reenginering of the code, this tactic has also been completely revised
+to get a very compact and readable version.} carries out rewritings according
+the rewriting rule bases {\tt \ident$_1$ \dots \ident$_n$}.
 
-A \emph{rewriting rule} is, by definition, a list of terms which type is an
-equality, each term being followed by the keyword \texttt{LR} (for
-left-to-right) or \texttt{RL} (for right-to-left):
+Each rewriting rule of a base \ident$_i$ is applied to the main subgoal until
+it fails. Once all the rules have been processed, if the main subgoal has
+progressed (e.g., if it is distinct from the initial main goal) then the rules
+of this base are processed again. If the main subgoal has not progressed then
+the next base is processed. For the bases, the behavior is exactly similar to
+the processing of the rewriting rules.
 
-\begin{tabular}{rcl}
-\rewrule & ::= & \texttt{[{\term} {\switch} {\dots} {\term} {\switch} ]}\\
-\switch & ::= & \texttt{LR}\\
-\switch & | & \texttt{RL} \\
-\end{tabular}
-
-\texttt{AutoRewrite} tries each rewriting of each rule, until 
-it succeeds; then the rewriting is processed and \texttt{AutoRewrite}
-tries again all rewritings from the first one. This tactic may not
-terminate and warnings are produced every 100 rewritings. 
+The rewriting rule bases are built with the {\tt Hint~Rewrite} vernacular
+command.
 
-\begin{Variants}
-\item {\tt AutoRewrite [\ident$_1$\dots\ \ident$_n$]
-Step=[\tac$_1$|...|\tac$_m$]}\\
-Each time a rewriting rule is successful, it tries to solve with the tactics of
-{\tt Step}.
-
-\item {\tt AutoRewrite [{\rewrule} {\dots} {\rewrule}]
-Step=[\tac$_1$|...|\tac$_m$] with Solve}\\
-This is equivalent to the previous variant.
-
-\item{\tt AutoRewrite [{\rewrule} {\dots} {\rewrule}]
-Step=[\tac$_1$|...|\tac$_m$] with Use}\\
-Each time a rewriting rule is successful, it tries to apply a tactic of {\tt
-Step}.
-
-\item{\tt AutoRewrite [{\rewrule} {\dots} {\rewrule}]
-Step=[\tac$_1$|...|\tac$_m$] with All}\\
-Each time a rewriting rule is successful, it tries to solve with the tactics of
-{\tt Step}, if it fails, it tries to apply a tactic of {\tt Step}. In fact, it
-behaves like the {\tt Solve} switch first and the {\tt Use} switch next in case
-of failure.
-
-\item {\tt AutoRewrite [{\rewrule} {\dots} {\rewrule}]
-Rest=[\tac$_1$|...|\tac$_m$]}\\
-If subgoals are generated by a conditional rewriting, it tries to solve each of
-them with the tactics in {\tt Rest}.
-
-\item {\tt AutoRewrite [{\rewrule} {\dots} {\rewrule}]
-Rest=[\tac$_1$|...|\tac$_m$] with Solve}\\
-This is equivalent to the previous variant.
-
-\item {\tt AutoRewrite [{\rewrule} {\dots} {\rewrule}]
-Rest=[\tac$_1$|...|\tac$_m$] with Cond}\\
-Each time subgoals are generated by a successful conditional rewriting, it
-tries to solve all of them, if it fails, it considers that the rewriting rule
-fails and takes the next one in the bases.
-
-\item {\tt AutoRewrite [{\rewrule} {\dots} {\rewrule}] Depth=\num}\\
-Produces a warning giving the number of rewritings carried out every {\num}
-rewritings.
-\end{Variants}
+\Warning{} This tactic may loop if you build non terminating rewriting systems.
 
-The three options {\tt Step}, {\tt Solve} et {\tt Depth} can be combined.
+\begin{Variant}
+\item {\tt AutoRewrite  [ \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.
+\end{Variant}
 
-\subsection{\tt HintRewrite {\ident} {\rewrule}}\comindex{HintRewrite}
+\subsection{\tt HintRewrite [ \term$_1$ \dots \term$_n$ ] in \ident}
+\comindex{HintRewrite}
 
-This vernacular command makes an alias for a rewriting rule.
-Then, instead of \texttt{AutoRewrite [{\rewrule} \dots ]} you can
-type: \texttt{AutoRewrite [{\ident} \dots ]}
+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 vernacular 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} declarations at the global
-level of that module are loaded.
+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}
+declarations at the global level of that module are loaded.
 
-\SeeAlso \ref{AutoRewrite-example} for examples showing the use of
-this tactic.
+\begin{Variants}
+\item {\tt HintRewrite -> [ \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}\\
+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}\\
+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.
+\end{Variants}
 
-\SeeAlso file \texttt{theories/DEMOS/DemoAutoRewrite.v}
+\SeeAlso \ref{AutoRewrite-example} for examples showing the use of this tactic.
 
+\SeeAlso file \texttt{contrib/Rocq/DEMOS/Demo\_AutoRewrite.v}
 
 \section{The hints databases for Auto and EAuto}
 \index{Hints databases}\label{Hints-databases}
diff --git a/doc/RefMan-tacex.tex b/doc/RefMan-tacex.tex
index 8e30077fbf..acb57e41a9 100644
--- a/doc/RefMan-tacex.tex
+++ b/doc/RefMan-tacex.tex
@@ -416,8 +416,15 @@ Reset Initial.
 \section{\tt AutoRewrite}
 \label{AutoRewrite-example}
 
-\Example
-Here is a basic use of {\tt AutoRewrite} with the Ackermann function:
+Here are two examples of {\tt AutoRewrite} use. The first one ({\em Ackermann
+function}) shows actually a quite basic use where there is no conditional
+rewriting. The second one ({\em Mac Carthy function}) involves conditional
+rewritings and shows how to deal with them using the optional tactic of the
+{\tt Hint~Rewrite} command.
+
+\firstexample
+\example{Ackermann function}
+%Here is a basic use of {\tt AutoRewrite} with the Ackermann function:
 
 \begin{coq_example*}
 Require Arith.
@@ -430,18 +437,18 @@ Axiom Ack2:(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 ] in base0.
 
-Lemma ResAck0:(Ack (2) (1))=(5).
-AutoRewrite [base0] using Trivial.
+Lemma ResAck0:(Ack (3) (2))=(29).
+AutoRewrite [ base0 ] using Try Reflexivity.
 \end{coq_example}
 
 \begin{coq_eval}
 Reset Initial.  
 \end{coq_eval}
 
-\Example
-The Mac Carthy function shows a more complex case:
+\example{Mac Carthy function}
+%The Mac Carthy function shows a more complex case:
 
 \begin{coq_example*}
 Require Omega.
@@ -450,48 +457,28 @@ Variable g:nat->nat->nat.
 
 Axiom g0:(m:nat)(g (0) m)=m.
 Axiom g1:
-  (n,m:nat)(gt n (0))->(gt m (100))->
-  (g n m)=(g (pred n) (minus m (10))).
-Axiom g2:
-  (n,m:nat)(gt n (0))->(le m (100))->(g n m)=(g (S n) (plus m (11))).
+  (n,m:nat)(gt n (0))->(gt m (100))->(g n m)=(g (pred n) (minus m (10))).
+Axiom g2:(n,m:nat)(gt n (0))->(le m (100))->(g n m)=(g (S n) (plus m (11))).
 \end{coq_example*}
 
 \begin{coq_example}
-Hint Rewrite -> [ g0 g1 ] in base1.
-Hint Rewrite -> [ g2 ] in base2.
-
-Lemma Resg0:(g (1) (90))=(91).
-AutoRewrite [base1 base2] 
-  Step=[Simpl|Reflexivity] with All
-  Rest=[Omega] with Cond 
-  Depth=10.
+Hint Rewrite [ g0 g1 g2 ] in base1 using Omega.
+
+Lemma Resg0:(g (1) (110))=(100).
+AutoRewrite [ base1 ] using Reflexivity Orelse Simpl.
 \end{coq_example}
-\begin{coq_eval}
-Abort.
-\end{coq_eval}
 
 \begin{coq_eval}
-Lemma maccarthy_90 : 
-  (g0:(m:nat)(g (0) m)=m)
-  (g1:(n,m:nat)(gt n (0))->(gt m (100))-> (g n m)=(g (pred n) (minus m (10))))
-  (g2:(n,m:nat)(gt n (0))->(le m (100))->(g n m)=(g (S n) (plus m (11))))
-  (g (1) (90))=(91).
-  Intros.
+Abort.
 \end{coq_eval}
 
-One can also give the full base definition instead of a name. This is
-useful to do rewritings with the hypotheses of current goal:
-
 \begin{coq_example}
-  Show.
-  AutoRewrite [[g0 LR g1 LR] [g2 LR]] 
-  Step=[Simpl|Reflexivity] with All
-  Rest=[Omega] with Cond 
-  Depth=10.
+Lemma Resg1:(g (1) (95))=(91).
+AutoRewrite [ base1 ] using Reflexivity Orelse Simpl.
 \end{coq_example}
 
 \begin{coq_eval}
-Abort.
+Reset Initial.
 \end{coq_eval}
 
 \section{\tt Quote}
diff --git a/doc/biblio.bib b/doc/biblio.bib
index 2e97d1e071..653944c9d3 100755
--- a/doc/biblio.bib
+++ b/doc/biblio.bib
@@ -618,6 +618,21 @@ of the {ML} language},
         YEAR               = {1990}
 }
 
+@INPROCEEDINGS{LTAC,
+  author    = "Delahaye, D.",
+  title     = "A {T}actic {L}anguage for the {S}ystem {{\sf Coq}}",
+  booktitle = "Proceedings of Logic for Programming and Automated Reasoning
+               (LPAR), Reunion Island",
+  publisher = "Springer-Verlag LNCS/LNAI",
+  volume    = "1955",
+  pages     = "85--95",
+  month     = "November",
+  year      = "2000",
+  note      =
+    "{\sf ftp://ftp.inria.fr/INRIA/Projects/coq/David.Delahaye/papers/}"#
+    "{\sf LPAR2000-ltac.ps.gz}"
+}
+
 @BOOK{MaL84,
         AUTHOR             = {{P. Martin-L\"of}},
         PUBLISHER          = {Bibliopolis},
@@ -776,6 +791,16 @@ the Calculus of Inductive Constructions}},
         YEAR               = {1993}
 }
 
+@BOOK{RC95,
+  author = "di~Cosmo, R.",
+  title  = "Isomorphisms of Types: from $\lambda$-calculus to information
+            retrieval and language design",
+  series = "Progress in Theoretical Computer Science",
+  publisher = "Birkhauser",
+  year = "1995",
+  note = "ISBN-0-8176-3763-X"
+}
+
 @TECHREPORT{Rou92,
         AUTHOR             = {J. Rouyer},
         INSTITUTION        = {INRIA},
diff --git a/doc/macros.tex b/doc/macros.tex
index 53c44176fb..1aff2c0836 100755
--- a/doc/macros.tex
+++ b/doc/macros.tex
@@ -71,6 +71,7 @@
 \newcommand{\gallina}{\textsf{Gallina}}
 \newcommand{\CIC}{\mbox{\sc Cic}}
 \newcommand{\FW}{\mbox{$F_{\omega}$}}
+\newcommand{\bn}{{\sf BNF}}
 
 %%%%%%%%%%%%%%%%%%%
 % Name of tactics %
@@ -205,6 +206,7 @@
 \newcommand{\Where}{{\textbf{where rec }}}
 \newcommand{\Function}{{\textbf{function }}}
 \newcommand{\Rec}{{\textbf{rec }}}
+\newcommand{\cn}{\centering}
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 % Math commands and symbols %