*** empty log message ***

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

7 files changed, 619 insertions, 731 deletions

diff --git a/doc/RefMan-gal.tex b/doc/RefMan-gal.tex
index 93b3d0f252..73250efd37 100644
--- a/doc/RefMan-gal.tex
+++ b/doc/RefMan-gal.tex
@@ -79,6 +79,7 @@ identifiers.
 Numerals are sequences of digits. Integers are numerals optionally preceded by a minus sign.
 
 \index{num@{\num}}
+\index{integer@{\integer}}
 \begin{center}
 \begin{tabular}{r@{\quad::=\quad}l}
 {\digit} & \ml{0..9} \\
@@ -88,9 +89,14 @@ Numerals are sequences of digits. Integers are numerals optionally preceded by a
 \end{center}
 
 \paragraph{Strings}
+\label{strings}
+\index{string@{\qstring}}
 Strings are delimited by \verb!"! (double quote), and enclose a
 sequence of any characters different from \verb!"! or the sequence
-\verb!""! to denote the double quote character.
+\verb!""! to denote the double quote character. In grammars, the
+entry for quoted strings is {\qstring}.
+
+
 %% \begin{center}
 %% \begin{tabular}{|l|l|}
 %% \hline
@@ -330,7 +336,9 @@ chapter \ref{Addoc-syntax}.
  & $|$ & {\tt fun} {\binderlist} {\tt =>} {\term} &(\ref{abstractions})\\
  & $|$ & {\tt fix} {\fixpointbodies} &(\ref{fixpoints})\\
  & $|$ & {\tt cofix} {\cofixpointbodies} &(\ref{fixpoints})\\
- & $|$ & {\tt let} {\letclauses} {\tt in} {\term} &(\ref{let-in})\\
+ & $|$ &
+    {\tt let} {\ident} \sequence{\binderlet}{} {\typecstr} {\tt :=} {\term}
+    {\tt in} {\term} &(\ref{let-in})\\
  & $|$ & {\tt let fix} {\fixpointbody} {\tt in} {\term} &(\ref{fixpoints})\\
  & $|$ & {\tt let cofix} {\cofixpointbody}
          {\tt in} {\term} &(\ref{fixpoints})\\
@@ -341,9 +349,11 @@ chapter \ref{Addoc-syntax}.
  & $|$ & {\term} {\tt :} {\term} &(\ref{typecast})\\
  & $|$ & {\term} {\tt ->} {\term} &(\ref{products})\\
  & $|$ & {\term} \nelist{\termarg}{}&(\ref{applications})\\
- & $|$ & {\tt @} {\qualid} \sequence{\term}{} &(\ref{applications})\\
+ & $|$ & {\tt @} {\qualid} \sequence{\term}{}
+            &(\ref{Implicits-explicitation})\\
  & $|$ & {\term} {\tt \%} {\ident} &(\ref{scopechange})\\
- & $|$ & {\tt match} {\caseitems} \zeroone{\casetype} {\tt with} &\\
+ & $|$ & {\tt match} \nelist{\caseitem}{\tt ,}
+                 \zeroone{\casetype} {\tt with} &\\
     &&   ~~~\zeroone{\zeroone{\tt |} \nelist{\eqn}{|}} {\tt end}
     &(\ref{caseanalysis})\\
  & $|$ & {\qualid} &(\ref{qualid})\\
@@ -352,8 +362,10 @@ chapter \ref{Addoc-syntax}.
  & $|$ & {\_} &(\ref{applications})\\
  & & &\\
 {\termarg} & ::= & {\term} &\\
- & $|$ & {\tt (} {\ident} {\tt :=} {\term} {\tt )} &\\
- & $|$ & {\tt (} {\num} {\tt :=} {\term} {\tt )} &\\
+ & $|$ & {\tt (} {\ident} {\tt :=} {\term} {\tt )}
+         &(\ref{Implicits-explicitation})\\
+ & $|$ & {\tt (} {\num} {\tt :=} {\term} {\tt )}
+         &(\ref{Implicits-explicitation})\\
 &&&\\
 {\binderlist} & ::= & \nelist{\name}{} {\typecstr} &\\
  & $|$ & {\binder} \nelist{\binderlet}{} &\\
@@ -362,12 +374,12 @@ chapter \ref{Addoc-syntax}.
 {\binderlet} & ::= & {\binder} &\\
  & $|$ & {\tt (} {\name} {\typecstr} {\tt :=} {\term} {\tt )} &\\
 & & &\\
-{\qualid} & ::= & {\ident} &\\
- & $|$ & {\qualid} {\accessident} &\\
- & & &\\
 {\name} & \cn{}::= & {\ident} &\\
  & $|$ & {\tt \_} &\\
 &&&\\
+{\qualid} & ::= & {\ident} &\\
+ & $|$ & {\qualid} {\accessident} &\\
+ & & &\\
 {\sort} & ::= & {\tt Prop} &\\
  & $|$ & {\tt Set} &\\
  & $|$ & {\tt Type} &\\
@@ -403,8 +415,6 @@ chapter \ref{Addoc-syntax}.
   & &\\
 {\annotation} & ::= & {\tt \{ struct} {\ident} {\tt \}} \\ 
 &&\\
-{\caseitems} & ::= & \nelist{\caseitem}{\tt ,} \\
-&&\\
 {\caseitem} & ::= & {\term} \zeroone{{\tt as} \name}
      \zeroone{{\tt in} \term} \\
 &&\\
@@ -436,7 +446,14 @@ denote local {\em variables}, what qualified identifiers do not.
 \subsection{Numerals}
 \label{numerals}
 
-%% TODO
+Numerals have no definite semantics in the calculus. They are mere
+notations that can be bound to objects through the notation mechanism
+(see chapter~\ref{Addoc-syntax} for details). Initially, numerals are
+bound to Peano's representation of natural numbers
+(see~\ref{libnats}).
+
+Note: negative integers are not at the same level as {\num}, for this
+would make precedence unnatural.
 
 \subsection{Sorts}\index{Sorts}
 \index{Type@{\Type}}
@@ -572,14 +589,14 @@ matched.
 \label{fixpoints}
 \index{fix@{fix \ident$_i$\{\dots\}}}
 
-The expression ``{\tt fix} \ident$_1$ \binders$_1$ {\tt :} {\type$_1$}
+The expression ``{\tt fix} \ident$_1$ \binder$_1$ {\tt :} {\type$_1$}
 \texttt{:=} \term$_1$ {\tt with} {\ldots} {\tt with} \ident$_n$
-\binders$_n$~{\tt :} {\type$_n$} \texttt{:=} \term$_n$ {\tt for}
+\binder$_n$~{\tt :} {\type$_n$} \texttt{:=} \term$_n$ {\tt for}
 {\ident$_i$}'' denotes the $i$th component of a block of functions
 defined by mutual well-founded recursion.
 
-The expression ``{\tt cofix} \ident$_1$~\binders$_1$ {\tt :}
-{\type$_1$} {\tt with} {\ldots} {\tt with} \ident$_n$ \binders$_n$
+The expression ``{\tt cofix} \ident$_1$~\binder$_1$ {\tt :}
+{\type$_1$} {\tt with} {\ldots} {\tt with} \ident$_n$ \binder$_n$
 {\tt :} {\type$_n$}~{\tt for} {\ident$_i$}'' denotes the $i$th
 component of a block of terms defined by a mutual guarded recursion.
 
diff --git a/doc/RefMan-lib.tex b/doc/RefMan-lib.tex
index b147fd659e..0d87023155 100755
--- a/doc/RefMan-lib.tex
+++ b/doc/RefMan-lib.tex
@@ -306,6 +306,8 @@ again defined as inductive constructions over the sort
 \index{Programming}
 \index{Datatypes}
 
+\label{libnats}
+
 \ttindex{unit}
 \ttindex{tt}
 \ttindex{bool}
diff --git a/doc/RefMan-ltac.tex b/doc/RefMan-ltac.tex
index 84ec732fbf..b7be362578 100644
--- a/doc/RefMan-ltac.tex
+++ b/doc/RefMan-ltac.tex
@@ -5,10 +5,12 @@
 
 This chapter gives a compact documentation of Ltac, the tactic
 language available in {\Coq}. We start by giving the syntax, and next,
-we present the informal semantics. 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{Del00}.
+we present the informal semantics. If you want to know more regarding
+this language and especially about its fundations, you can refer
+to~\cite{Del00}. Chapter~\ref{Tactics-examples} is devoted to giving
+examples of use of this language on small but also with non-trivial
+problems.
+
 
 \section{Syntax}
 
@@ -22,29 +24,49 @@ you can refer to~\cite{Del00}.
 \def\matchrule{\textrm{\textsl{match\_rule}}}
 \def\contextrule{\textrm{\textsl{context\_rule}}}
 \def\contexthyps{\textrm{\textsl{context\_hyps}}}
-\def\primitivetactic{\textrm{\textsl{primitive\_tactic}}}
-\def\tacarg{\textrm{\textsl{arg}}}
-\def\qstring{\textrm{\textsl{string}}}
+\def\tacarg{\nterm{tacarg}}
 \def\cpattern{\nterm{cpattern}}
 
 The syntax of the tactic language is given in tables~\ref{ltac}
 and~\ref{ltac_aux}. See section~\ref{BNF-syntax} for a description of
 the BNF metasyntax used in these tables. Various already defined
 entries will be used in this chapter: entries {\naturalnumber},
-{\integer}, {\ident}, {\qualid}, {\term}, {\cpattern} and
-{\primitivetactic} represent respectively the natural and integer
-numbers, the authorized identificators and qualified names, {\Coq}'s
-terms and patterns and all the basic tactics. The syntax of
-{\cpattern} is the same as that of terms, but there can
-be specific variables like {\tt ?id} where {\tt id} is a {\ident} or
-{\tt \_}, which are metavariables for pattern matching. {\tt ?id} allows
-us to keep instantiations and to make constraints whereas {\tt \_}
-shows that we are not interested in what will be matched. On the right
-hand side, they are used without the question mark.
+{\integer}, {\ident}, {\qualid}, {\term}, {\cpattern} and {\atomictac}
+represent respectively the natural and integer numbers, the authorized
+identificators and qualified names, {\Coq}'s terms and patterns and
+all the atomic tactics described in chapter~\ref{Tactics}. The syntax
+of {\cpattern} is the same as that of terms, but there can be specific
+variables like {\tt ?id} where {\tt id} is a {\ident} or {\tt \_},
+which are metavariables for pattern matching. {\tt ?id} allows us to
+keep instantiations and to make constraints whereas {\tt \_} shows
+that we are not interested in what will be matched. On the right hand
+side, they are used without the question mark.
 
 The main entry of the grammar is {\tacexpr}. This language is used in
 proof mode but it can also be used in toplevel definitions as shown in
 table~\ref{ltactop}.
+\begin{Remarks}
+\item The infix tacticals ``\dots\ {\tt ||} \dots'' and ``\dots\ {\tt
+    ;} \dots'' are associative. 
+
+\item As shown by the figure, tactical {\tt ||} binds more than the
+prefix tacticals {\tt try}, {\tt repeat}, {\tt do}, {\tt info} and
+{\tt abstract} which themselves bind more than the postfix tactical
+``{\tt \dots\ ;[ \dots\ ]}'' which binds more than ``\dots\ {\tt ;}
+\dots''.
+
+For instance
+\begin{tabbing}
+{\tt try repeat \tac$_1$ ||
+  \tac$_2$;\tac$_3$;[\tac$_{31}$|\dots|\tac$_{3n}$];\tac$_4$.}
+\end{tabbing}
+is understood as 
+\begin{tabbing}
+{\tt (try (repeat (\tac$_1$ || \tac$_2$)));} \\
+{\tt ((\tac$_3$;[\tac$_{31}$|\dots|\tac$_{3n}$]);\tac$_4$).}
+\end{tabbing}
+\end{Remarks}
+
 
 \begin{table}[htbp]
 \noindent{}\framebox[6in][l]
@@ -93,7 +115,7 @@ table~\ref{ltactop}.
 & \cn{}| & {\tt eval} {\nterm{redexpr}} {\tt in} {\term}\\
 & \cn{}| & {\tt type of} {\term}\\
 & \cn{}| & {\tt constr :} {\term}\\
-& \cn{}| & \primitivetactic\\
+& \cn{}| & \atomictac\\
 & \cn{}| & {\qualid} \nelist{\tacarg}{}\\
 & \cn{}| & {\atom}\\
 \\
@@ -157,7 +179,12 @@ table~\ref{ltactop}.
 \label{ltactop}
 \end{table}
 
+
+%%
+%% Semantics
+%%
 \section{Semantics}
+\index[tactic]{Tacticals}\index{Tacticals}\label{Tacticals}
 
 Tactic expressions can only be applied in the context of a goal.  The
 evaluation yields either a term, an integer or a tactic. Intermediary
@@ -217,6 +244,8 @@ of Ltac.
 
 \subsubsection{Sequence}
 \tacindex{;}
+\index{;@{\tt ;}}
+\index{Tacticals!;@{\tt {\tac$_1$};\tac$_2$}}
 
 A sequence is an expression of the following form:\\
 
@@ -224,11 +253,13 @@ A sequence is an expression of the following form:\\
 
 {\tacexpr}$_1$ and {\tacexpr}$_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
+and $v_2$ is applied to every subgoal generated by the application of
 $v_1$. Sequence is left associating.
 
 \subsubsection{General sequence}
 \tacindex{; [ | ]}
+\index{; [ | ]@{\tt ;[\ldots$\mid$\ldots$\mid$\ldots]}}
+\index{Tacticals!; [ | ]@{\tt {\tac$_0$};[{\tac$_1$}$\mid$\ldots$\mid$\tac$_n$]}}
 
 We can generalize the previous sequence operator by:\\
 
@@ -242,18 +273,21 @@ $v_0$ does not generate exactly $n$ subgoals.
 
 \subsubsection{For loop}
 \tacindex{do}
+\index{Tacticals!do@{\tt do}}
 
-We have a for loop with:\\
+There is a for loop that repeats a tactic {\num} times:\\
 
-{\tt do} $n$ {\tacexpr}\\
+{\tt do} {\num} {\tacexpr}\\
 
-{\tacexpr} 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.
+{\tacexpr} is evaluated to $v$. $v$ must be a tactic value. $v$ is
+applied {\num} times. Supposing ${\num}>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 {\num} applications have been completed.
 
 \subsubsection{Repeat loop}
 \tacindex{repeat}
+\index{Tacticals!repeat@{\tt repeat}}
 
 We have a repeat loop with:\\
 
@@ -267,6 +301,7 @@ fails.
 
 \subsubsection{Error catching}
 \tacindex{try}
+\index{Tacticals!try@{\tt try}}
 
 We can catch the tactic errors with:\\
 
@@ -289,12 +324,12 @@ applied. If the application of $v$ produced one subgoal equal to the
 initial goal (up to syntactical equality), then an error of level 0 is
 raised. 
 
-{\tt Error message:}\\
+\ErrMsg \errindex{Failed to progress}
 
-\errindex{Failed to progress}
 
 \subsubsection{Branching}
 \tacindex{||}
+\index{Tacticals!orelse@{\tt ||}}
 
 We can easily branch with the following structure:\\
 
@@ -305,6 +340,8 @@ $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{First tactic to work}
+\tacindex{first}
+\index{Tacticals!first@{\tt first}}
 
 We may consider the first tactic to work (i.e. which does not fail) among a
 panel of tactics:\\
@@ -315,11 +352,11 @@ panel of tactics:\\
 $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.\\
 
-{\tt Error message:}\\
-
-{\tt No applicable tactic}
+\ErrMsg \errindex{No applicable tactic}
 
 \subsubsection{Solving}
+\tacindex{solve}
+\index{Tacticals!solve@{\tt solve}}
 
 We may consider the first to solve (i.e. which generates no subgoal) among a
 panel of tactics:\\
@@ -330,37 +367,36 @@ panel of tactics:\\
 $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.\\
 
-{\tt Error message:}\\
-
-{\tt Cannot solve the goal}
+\ErrMsg \errindex{Cannot solve the goal}
 
 \subsubsection{Identity}
+\tacindex{idtac}
+\index{Tacticals!idtac@{\tt idtac}}
 
-We have the identity tactic:\\
+The constant {\tt idtac} is the identity tactic: it leaves any goal
+unchanged but it appears in the proof script.\\
 
 {\tt idtac} and {\tt idtac "message"}\\
 
-It leaves the goal unchanged but it appears in the proof script.
-If there is a string as argument then it prints this string on the
-standard output. 
+The latter variant prints the string on the standard output.
 
 \subsubsection{Failing}
+\tacindex{fail}
+\index{Tacticals!fail@{\tt fail}}
 
-We have the failing tactic:\\
+The tactic {\tt fail} is the always-failing tactic: it does not solve
+any goal. It is useful for defining other tacticals since it can be
+catched by {\tt try} or {\tt match goal}. There are three variants:\\
 
-{\tt fail}, {\tt fail $n$}, {\tt fail "message"}
- and {\tt fail $n$ "message"}  \\
+{\tt fail $n$}, {\tt fail "message"} and {\tt fail $n$ "message"}  \\
 
-It always fails and leaves the goal unchanged. It does not appear in
-the proof script and can be catched by {\tt try}. The number $n$ is
-the failure level. If no level is specified, it defaults to $0$.  The
-level is used in {\tt match goal}.  If $0$, it makes {\tt match
-goal} considering the next clause. If non zero, the current {\tt
-match goal} block is aborted and the level is decremented.
+The number $n$ is the failure level. If no level is specified, it
+defaults to $0$.  The level is used by {\tt try} and {\tt match goal}.
+If $0$, it makes {\tt match goal} considering the next clause
+(backtracking). If non zero, the current {\tt match goal} block or
+{\tt try} command is aborted and the level is decremented.
 
-{\tt Error message:}\\
-
-\errindex{Tactic Failure "message" (level $n$)}.
+\ErrMsg \errindex{Tactic Failure "message" (level $n$)}.
 
 \subsubsection{Local definitions}
 \tacindex{let}
@@ -443,15 +479,12 @@ immediately applied to the current goal (in contrast with {\tt match
 goal}). If all clauses fail (in particular, there is no pattern {\_})
 then a no-matching error is raised. \\
 
-{\tt Error messages:}\\
-
-\errindex{No matching clauses for match}
-
+\begin{ErrMsgs}
+\item \errindex{No matching clauses for match}\\
 \hx{4}No pattern can be used and, in particular, there is no {\tt \_} pattern.
-
-\errindex{Argument of match does not evaluate to a term}
-
+\item \errindex{Argument of match does not evaluate to a term}\\
 \hx{4}This happens when {\tacexpr} does not denote a term.
+\end{ErrMsgs}
 
 \tacindex{context (in pattern)}
 There is a special form of patterns to match a subterm against the
@@ -506,10 +539,7 @@ pattern is tried and so on. If the next to last proof context pattern
 fails then {\tacexpr}$_{n+1}$ is evaluated to $v_{n+1}$ and $v_{n+1}$
 is applied.\\
 
-{\tt Error message:}\\
-
-\errindex{No matching clauses for match goal}
-
+\ErrMsg \errindex{No matching clauses for match goal}\\
 \hx{4}No goal pattern can be used and, in particular, there is no {\tt
 \_} goal pattern.
 
@@ -535,10 +565,7 @@ pattern of a {\tt match} expression. This expression evaluates
 replaces the hole of the value of {\ident} by the value of
 {\tacexpr}.
 
-{\tt Error message:}\\
-
-\errindex{not a context variable}
-
+\ErrMsg \errindex{not a context variable}
 
 \subsubsection{Generating fresh hypothesis names}
 \tacindex{fresh}
@@ -577,32 +604,33 @@ hnf}, {\tt compute}, {\tt simpl}, {\tt cbv}, {\tt lazy}, {\tt unfold},
 
 \subsubsection{Accessing tactic decomposition}
 \tacindex{info}
+\index{Tacticals!info@{\tt info}}
 
-It is possible to print on standard output how a tactic was
-decomposed with:\\
+Tactical ``{\tt info} {\tacexpr}'' is not really a tactical. For
+elementary tactics, this is equivalent to \tacexpr. For complex tactic
+like \texttt{auto}, it displays the operations performed by the
+tactic.
 
-{\tt info} {\tacexpr}\\
 
-This may be useful to know what steps an automatic tactic made.
-
-
-\subsubsection{Making a subproof as a separate lemma}
+\subsubsection{Proving a subgoal as a separate lemma}
 \tacindex{abstract}
+\index{Tacticals!abstract@{\tt abstract}}
+From the outside ``\texttt{abstract \tacexpr}'' is the same as
+{\tt solve \tacexpr}. Internally it saves an auxiliary lemma called 
+{\ident}\texttt{\_subproof}\textit{n} where {\ident} is the name of the
+current goal and \textit{n} is chosen so that this is a fresh name.
 
-This tactical was made to avoid efficiency problems with huge proof
-terms. It allows to prove the current goal as a separate lemma by
-applying a tactic. This tactic is supposed to solve the goal.
-
-{\tt abstract} {\tacexpr} {\tt using} {\ident}
-
-Creates a constant {\ident} (if not provided, a fresh name is
-generated by the tactical), which type is the current goal and applies
-{\tacexpr} on it.
+This tactical is useful with tactics such as \texttt{omega} or
+\texttt{discriminate} that generate huge proof terms. With that tool
+the user can avoid the explosion at time of the \texttt{Save} command
+without having to cut manually the proof in smaller lemmas.
 
-{\tt Error messages:}
-
-\errindex{Proof is not complete}
+\begin{Variants}
+\item \texttt{abstract {\tacexpr} using {\ident}}.\\
+  Give explicitly the name of the auxiliary lemma.
+\end{Variants}
 
+\ErrMsg \errindex{Proof is not complete}
 
 \subsection{Tactic toplevel definitions}
 \comindex{Ltac}
@@ -646,400 +674,4 @@ possible with the syntax:
 %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{coq_eval}
-Reset Initial.
-Require Import Arith.
-Require Import List.
-\end{coq_eval}
-
-\begin{table}[ht]
-\noindent{}\framebox[6.4in][l]
-{\parbox{6.4in}
-{
-\begin{coq_example*}
-Lemma card_nat :
- ~ (exists x : nat, exists y : nat, forall z:nat, x = z \/ y = z).
-Proof.
-red; intros (x, (y, Hy)).
-elim (Hy 0); elim (Hy 1); elim (Hy 2); intros;
- match goal with
- | [_:(?a = ?b),_:(?a = ?c) |- _ ] =>
-     cut (b = c); [ discriminate | apply trans_equal with a; auto ]
- end.
-Qed.
-\end{coq_example*}
-}}
-\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 {\tt match goal} structure and, in particular, with only one pattern (use
-of non-linear matching).
-
-\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[6.4in][l]
-{\parbox{6.4in}
-{
-\begin{coq_example*}
-Section Sort.
-Variable A : Set.
-Inductive permut : list A -> list A -> Prop :=
-  | permut_refl   : forall l, permut l l
-  | permut_cons   :
-      forall a l0 l1, permut l0 l1 -> permut (a :: l0) (a :: l1)
-  | permut_append : forall a l, permut (a :: l) (l ++ a :: nil)
-  | permut_trans  :
-      forall l0 l1 l2, permut l0 l1 -> permut l1 l2 -> permut l0 l2.
-End Sort.
-\end{coq_example*}
-}}
-\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 {\tt
-PermutProve} and {\tt Permut}. The function to be called is {\tt PermutProve}
-which computes the lengths of the two lists and calls {\tt Permut} with the
-length if the two lists have the same length. {\tt Permut} works as expected.
-If the two lists are equal, it concludes. Otherwise, if the lists have
-identical first elements, it applies {\tt 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 {\tt 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 {\tt 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 {\tt eval
-compute in} and we can get the terms back by {\tt match}.
- 
-\begin{table}[p]
-\noindent{}\framebox[6.4in][l]
-{\parbox{6.4in}
-{
-\begin{coq_example}
-Ltac Permut n :=
-  match goal with
-  | |- (permut _ ?l ?l) => apply permut_refl
-  | |- (permut _ (?a :: ?l1) (?a :: ?l2)) =>
-      let newn := eval compute in (length l1) in
-      (apply permut_cons; Permut newn)
-  | |- (permut ?A (?a :: ?l1) ?l2) =>
-      match eval compute in n with
-      | 1 => fail
-      | _ =>
-          let l1' := constr:(l1 ++ a :: nil) in
-          (apply (permut_trans A (a :: l1) l1' l2);
-            [ apply permut_append | compute; Permut (pred n) ])
-      end
-  end.
-Ltac PermutProve :=
-  match goal with
-  | |- (permut _ ?l1 ?l2) =>
-      match eval compute in (length l1 = length l2) with
-      | (?n = ?n) => Permut n
-      end
-  end.
-\end{coq_example}
-}}
-\caption{Permutation tactic}
-\label{permutltac}
-\end{table}
-
-With {\tt PermutProve}, we can now prove lemmas such those shown in
-table~\ref{permutlem}.
-
-\begin{table}[p]
-\noindent{}\framebox[6.4in][l]
-{\parbox{6.4in}
-{
-\begin{coq_example*}
-Lemma permut_ex1 :
-  permut nat (1 :: 2 :: 3 :: nil) (3 :: 2 :: 1 :: nil).
-Proof.
-PermutProve.
-Qed.
-
-Lemma permut_ex2 :
-  permut nat
-    (0 :: 1 :: 2 :: 3 :: 4 :: 5 :: 6 :: 7 :: 8 :: 9 :: nil)
-    (0 :: 2 :: 4 :: 6 :: 8 :: 9 :: 7 :: 5 :: 3 :: 1 :: nil).
-Proof.
-PermutProve.
-Qed.
-\end{coq_example*}
-}}
-\caption{Examples of {\tt PermutProve} use}
-\label{permutlem}
-\end{table}
-
-\subsection{Deciding intuitionistic propositional logic}
-
-The pattern matching on goals allows a complete and so a powerful
-backtracking when returning tactic values. An interesting application
-is the problem of deciding intuitionistic propositional
-logic. Considering the contraction-free sequent calculi {\tt 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 {\tt Axioms} tries to conclude using usual axioms. The tactic
-{\tt DSimplif} applies all the reversible rules of Dyckhoff's
-system. Finally, the tactic {\tt TautoProp} (the main tactic to be
-called) simplifies with {\tt DSimplif}, tries to conclude with {\tt
-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[6.4in][l]
-{\parbox{6.4in}
-{
-\begin{coq_example}
-Ltac Axioms :=
-  match goal with
-  | |- True => trivial
-  | _:False |- _  => elimtype False; assumption
-  | _:?A |- ?A  => auto
-  end.
-Ltac DSimplif :=
-  repeat
-   (intros;
-    match goal with
-     | id:(~ _) |- _ => red in id
-     | id:(_ /\ _) |- _ =>
-         elim id; do 2 intro; clear id
-     | id:(_ \/ _) |- _ =>
-         elim id; intro; clear id
-     | id:(?A /\ ?B -> ?C) |- _ =>
-         cut (A -> B -> C);
-          [ intro | intros; apply id; split; assumption ]
-     | id:(?A \/ ?B -> ?C) |- _ =>
-         cut (B -> C);
-          [ cut (A -> C);
-             [ intros; clear id
-             | intro; apply id; left; assumption ]
-          | intro; apply id; right; assumption ]
-     | id0:(?A -> ?B),id1:?A |- _ =>
-         cut B; [ intro; clear id0 | apply id0; assumption ]
-     | |- (_ /\ _) => split
-     | |- (~ _) => red
-     end).
-Ltac TautoProp :=
-  DSimplif;
-   Axioms ||
-     match goal with
-     | id:((?A -> ?B) -> ?C) |- _ =>
-          cut (B -> C);
-          [ intro; cut (A -> B);
-             [ intro; cut C;
-                [ intro; clear id | apply id; assumption ]
-             | clear id ]
-          | intro; apply id; intro; assumption ]; TautoProp
-     | id:(~ ?A -> ?B) |- _ =>
-         cut (False -> B);
-          [ intro; cut (A -> False);
-             [ intro; cut B;
-                [ intro; clear id | apply id; assumption ]
-             | clear id ]
-          | intro; apply id; red; intro; assumption ]; TautoProp
-     | |- (_ \/ _) => (left; TautoProp) || (right; TautoProp)
-     end.
-\end{coq_example}
-}}
-\caption{Deciding intuitionistic propositions}
-\label{tautoltac}
-\end{table}
-
-For example, with {\tt TautoProp}, we can prove tautologies like those in
-table~\ref{tautolem}.
-
-\begin{table}[ht]
-\noindent{}\framebox[6.4in][l]
-{\parbox{6.4in}
-{
-\begin{coq_example*}
-Lemma tauto_ex1 : forall A B:Prop, A /\ B -> A \/ B.
-Proof.
-TautoProp.
-Qed.
-
-Lemma tauto_ex2 :
-   forall A B:Prop, (~ ~ B -> B) -> (A -> B) -> ~ ~ A -> B.
-Proof.
-TautoProp.
-Qed.
-\end{coq_example*}
-}}
-\caption{Proofs of tautologies with {\tt 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[6.4in][l]
-{\parbox{6.4in}
-{
-\begin{coq_eval}
-Reset Initial.
-\end{coq_eval}
-\begin{coq_example*}
-Open Scope type_scope.
-Section Iso_axioms.
-Variables A B C : Set.
-Axiom Com : A * B = B * A.
-Axiom Ass : A * (B * C) = A * B * C.
-Axiom Cur : (A * B -> C) = (A -> B -> C).
-Axiom Dis : (A -> B * C) = (A -> B) * (A -> C).
-Axiom P_unit : A * unit = A.
-Axiom AR_unit : (A -> unit) = unit.
-Axiom AL_unit : (unit -> A) = A.
-Lemma Cons : B = C -> A * B = A * C.
-Proof.
-intro Heq; rewrite Heq; apply refl_equal.
-Qed.
-End Iso_axioms.
-\end{coq_example*}
-}}
-\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 {\tt
-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 {\tt
-CompareStruct}). The main tactic to be called and realizing this algorithm is
-{\tt IsoProve}.
-
-\begin{table}[ht]
-\noindent{}\framebox[6.4in][l]
-{\parbox{6.4in}
-{
-\begin{coq_example}
-Ltac DSimplif trm :=
-  match trm with
-  | (?A * ?B * ?C) =>
-      rewrite <- (Ass A B C); try MainSimplif
-  | (?A * ?B -> ?C) =>
-      rewrite (Cur A B C); try MainSimplif
-  | (?A -> ?B * ?C) =>
-      rewrite (Dis A B C); try MainSimplif
-  | (?A * unit) =>
-      rewrite (P_unit A); try MainSimplif
-  | (unit * ?B) =>
-      rewrite (Com unit B); try MainSimplif
-  | (?A -> unit) =>
-      rewrite (AR_unit A); try MainSimplif
-  | (unit -> ?B) =>
-      rewrite (AL_unit B); try MainSimplif
-  | (?A * ?B) =>
-      (DSimplif A; try MainSimplif) || (DSimplif B; try MainSimplif)
-  | (?A -> ?B) =>
-      (DSimplif A; try MainSimplif) || (DSimplif B; try MainSimplif)
-  end
- with MainSimplif :=
-  match goal with
-  | |- (?A = ?B) => try DSimplif A; try DSimplif B
-  end.
-Ltac Length trm :=
-  match trm with
-  | (_ * ?B) => let succ := Length B in constr:(S succ)
-  | _ => constr:1
-  end.
-Ltac assoc := repeat rewrite <- Ass.
-\end{coq_example}
-}}
-\caption{Type isomorphism tactic (1)}
-\label{isosltac1}
-\end{table}
-
-\begin{table}[ht]
-\noindent{}\framebox[6.4in][l]
-{\parbox{6.4in}
-{
-\begin{coq_example}
-Ltac DoCompare n :=
-  match goal with
-  | [ |- (?A = ?A) ] => apply refl_equal
-  | [ |- (?A * ?B = ?A * ?C) ] =>
-      apply Cons; let newn := Length B in
-                  DoCompare newn
-  | [ |- (?A * ?B = ?C) ] =>
-      match eval compute in n with
-      | 1 => fail
-      | _ =>
-          pattern (A * B) at 1; rewrite Com; assoc; DoCompare (pred n)
-      end
-  end.
-Ltac CompareStruct :=
-  match goal with
-  | [ |- (?A = ?B) ] =>
-      let l1 := Length A
-      with l2 := Length B in
-      match eval compute in (l1 = l2) with
-      | (?n = ?n) => DoCompare n
-      end
-  end.
-Ltac IsoProve := MainSimplif; CompareStruct.
-\end{coq_example}
-}}
-\caption{Type isomorphism tactic (2)}
-\label{isosltac2}
-\end{table}
-
-Table~\ref{isoslem} gives examples of what can be solved by {\tt IsoProve}.
-
-\begin{table}[ht]
-\noindent{}\framebox[6.4in][l]
-{\parbox{6.4in}
-{
-\begin{coq_example*}
-Lemma isos_ex1 : 
-  forall A B:Set, A * unit * B = B * (unit * A).
-Proof.
-intros; IsoProve.
-Qed.
-
-Lemma isos_ex2 :
-  forall A B C:Set,
-    (A * unit -> B * (C * unit)) =
-    (A * unit -> (C -> unit) * C) * (unit -> A -> B).
-Proof.
-intros; IsoProve.
-Qed.
-\end{coq_example*}
-}}
-\caption{Type equalities solved by {\tt IsoProve}}
-\label{isoslem}
-\end{table}
diff --git a/doc/RefMan-tac.tex b/doc/RefMan-tac.tex
index 75a9089216..b4cd2c9dd5 100644
--- a/doc/RefMan-tac.tex
+++ b/doc/RefMan-tac.tex
@@ -30,78 +30,29 @@ used to reduce any goal. In other words, before applying a tactic to a
 given goal, the system checks that some {\em preconditions} are
 satisfied. If it is not the case, the tactic raises an error message.
 
-Tactics are build from tacticals and atomic tactics.  There are, at
-least, three levels of atomic tactics. The simplest one implements
-basic rules of the logical framework. The second level is the one of
-{\em derived rules} which are built by combination of other
+Tactics are build from atomic tactics and tactic expressions (which
+extends the folklore notion of tactical) to combine those atomic
+tactics. This chapter is devoted to atomic tactics. The tactic
+language will be descrbed in chapter~\ref{TacticLanguage}.
+
+There are, at least, three levels of atomic tactics. The simplest one
+implements basic rules of the logical framework. The second level is
+the one of {\em derived rules} which are built by combination of other
 tactics. The third one implements heuristics or decision procedures to
-build a complete proof of a goal.  
-%Here is a table of all existing atomic tactics in \Coq:
-%\index{atomic tactics}
-%\label{atomic-tactics-table}
+build a complete proof of a goal.
 
-\section{Syntax of tactics and tacticals}
+\section{Invokation of tactics}
 \label{tactic-syntax}
 \index{tactic@{\tac}}
 
-A tactic is
-applied as an ordinary command. If the tactic does not
-address the first subgoal, the command may be preceded by the
-wished subgoal number. See figure~\ref{InvokeTactic} for the syntax of
-tactic invocation and tacticals.
+A tactic is applied as an ordinary command. If the tactic does not
+address the first subgoal, the command may be preceded by the wished
+subgoal number as shown below:
 
-\medskip
-
-\begin{figure}[t]
-\begin{center}
-\fbox{\begin{minipage}{0.95\textwidth}
 \begin{tabular}{lcl}
-{\tac} & ::= & \atomictac\\
-  & $|$ & {\tt (} {\tac} {\tt )} \\
-  & $|$ & {\tac} {\tt ||} {\tac}\\
-  & $|$ & {\tt repeat} \tac \\
-  & $|$ & {\tt do} {\num} {\tac} \\
-  & $|$ & {\tt info} \tac \\
-  & $|$ & {\tt try} \tac \\
-  & $|$ & {\tt first [} {\tac}{\tt\ | \dots\ | }{\tac} {\tt ]} \\
-  & $|$ & {\tt solve [} {\tac}{\tt\ | \dots\ | }{\tac} {\tt ]} \\
-  & $|$ & {\tt abstract} {\tac} \\
-  & $|$ & {\tt abstract} {\tac} {\tt using} {\ident}\\
-  & $|$ & {\tac} {\tt ;} {\tac}\\
-  & $|$ & {\tac} {\tt ;[} {\tac} \tt {\tt |}
-          \dots\ {\tt |} {\tac} {\tt ]} \\
 {\commandtac} & ::= & {\num} {\tt :} {\tac} {\tt .}\\
  & $|$ & {\tac} {\tt .}
 \end{tabular}
-\end{minipage}}
-\end{center}
-\caption{Invocation of tactics and tacticals}
-\label{InvokeTactic}
-\end{figure}
-
-\begin{Remarks}
-\item The infix tacticals ``\dots\ {\tt ||} \dots'' and ``\dots\ {\tt
-    ;} \dots'' are associative. 
-The tactical {\tt ||} binds more than the prefix tacticals
-{\tt try}, {\tt repeat}, {\tt do}, {\tt info} and {\tt abstract} which
-themselves bind more than  
-the postfix tactical ``{\tt \dots\ ;[ \dots\ ]}'' which 
-binds more than ``\dots\ {\tt ;} \dots''.
-
-For instance
-\begin{tabbing}
-{\tt try repeat \tac$_1$ ||
-  \tac$_2$;\tac$_3$;[\tac$_{31}$|\dots|\tac$_{3n}$];\tac$_4$.}
-\end{tabbing}
-is understood as 
-\begin{tabbing}
-{\tt (try (repeat (\tac$_1$ || \tac$_2$)));} \\
-{\tt ((\tac$_3$;[\tac$_{31}$|\dots|\tac$_{3n}$]);\tac$_4$).}
-\end{tabbing}
-
-
-\item An {\atomictac} is any of the tactics listed below.
-\end{Remarks}
 
 \section{Explicit proof as a term}
 
@@ -159,7 +110,7 @@ proved. Otherwise, it fails.
 \item  \errindex{No such assumption}
 \end{ErrMsgs}
 
-\subsection{\tt clear {\ident}.}\tacindex{clear}\label{clear}
+\subsection{\tt clear {\ident}}\tacindex{clear}\label{clear}
 This tactic erases the hypothesis named {\ident} in the local context
 of the current goal. Then {\ident} is no more displayed and no more
 usable in the proof development.
@@ -179,7 +130,8 @@ body. Otherwise said, this tactic turns a definition into an assumption.
 \item \errindex{{\ident} is used in the hypothesis {\ident'}}
 \end{ErrMsgs}
 
-\subsection{\tt move {\ident$_1$} after {\ident$_2$}.}\tacindex{Move}
+\subsection{\tt move {\ident$_1$} after {\ident$_2$}}
+\tacindex{Move}
 This moves the hypothesis named {\ident$_1$} in the local context
 after the hypothesis named {\ident$_2$}.
 
@@ -200,7 +152,8 @@ then all hypotheses between {\ident$_1$} and {\ident$_2$} which
                    it depends on {\ident$_2$}}
 \end{ErrMsgs}
 
-\subsection{\tt rename {\ident$_1$} into {\ident$_2$}.}\tacindex{Rename}
+\subsection{\tt rename {\ident$_1$} into {\ident$_2$}}
+\tacindex{Rename}
 This renames hypothesis {\ident$_1$} into {\ident$_2$} in the current
 context\footnote{but it does not rename the hypothesis in the
 proof-term...}
@@ -400,26 +353,28 @@ instantiations of the premises of the type of {\term}.
 
 \end{Variants}
 
-\subsection{\tt LetTac {\ident} {\tt :=} {\term}}\tacindex{LetTac}
+\subsection{{\tt set ( {\ident} {\tt :=} {\term} \tt )}}
+\tacindex{set}
 
-This replaces {\term} by {\ident} in the conclusion and the hypotheses
-of the current goal and adds the new definition {\ident {\tt :=}
-  \term} to the local context.
+This replaces {\term} by {\ident} in the conclusion or in the
+hypotheses of the current goal and adds the new definition {\ident
+{\tt :=} \term} to the local context. The default is to make this
+replacement only in the conclusion.
 
 \begin{Variants}
 
-\item {\tt LetTac {\ident} {\tt :=} {\term} {\tt in} {\tt Goal}}
+\item {\tt set ( } {\ident} {\tt :=} {\term} {\tt ) in *}
   
-  This is equivalent to the above form but applies only to the
-  conclusion of the goal.
+  This is equivalent to the above form but applies everywhere in the
+  goal (both in conclusion and hypotheses).
 
-\item {\tt LetTac {\ident$_0$} {\tt :=} {\term} {\tt in} {\ident$_1$}}
+\item {\tt set ( {\ident$_0$} {\tt :=} {\term} {\tt ) in} {\ident$_1$}}
   
   This behaves the same but substitutes {\term} not in the goal but in
   the hypothesis named {\ident$_1$}.
   
-\item {\tt LetTac {\ident$_0$} {\tt :=} {\term} {\tt in} {\num$_1$}
-    \dots\ {\num$_n$} {\ident$_1$}}
+\item {\tt set (} {\ident$_0$} {\tt :=} {\term} {\tt ) in}
+    {\ident$_1$} {\tt at} {\num$_1$} \dots\ {\num$_n$}
 
 This notation allows to specify which occurrences of the hypothesis
 named {\ident$_1$} (or the goal if {\ident$_1$} is the word {\tt
@@ -427,31 +382,35 @@ named {\ident$_1$} (or the goal if {\ident$_1$} is the word {\tt
 to right. A negative occurrence number means an occurrence which
 should not be substituted.
 
-\item {\tt LetTac {\ident$_0$} {\tt :=} {\term} {\tt in} {\num$_1^1$}
-    \dots\ {\num$_{n_1}^1$} {\ident$_1$} \dots {\num$_1^m$} \dots\ 
-    {\num$_{n_m}^m$} {\ident$_m$}}
+\item {\tt set (} {\ident$_0$} {\tt :=} {\term} {\tt ) in}
+    {\ident$_1$} {\tt at} {\num$_1^1$} \dots\ {\num$_{n_1}^1$} \dots
+    {\ident$_m$} {\tt at} {\num$_1^m$} \dots {\num$_{n_m}^m$}
   
   This is the general form. It substitutes {\term} at occurrences
   {\num$_1^i$} \dots\ {\num$_{n_i}^i$} of hypothesis {\ident$_i$}. One
   of the {\ident}'s may be the word {\tt Goal}.
 
-\item{\tt Pose {\ident} := {\term}}\tacindex{Pose}
+
+\item {\tt pose (  {\ident} {\tt :=} {\term} {\tt )}}
+\tacindex{pose}
+
+  This is equivalent to the default behaviour in {\tt set}.
   
-  This adds the local definition {\ident} := {\term} to the current
-  context without performing any replacement in the goal or in the
-  hypotheses.
+%  This adds the local definition {\ident} := {\term} to the current
+%  context without performing any replacement in the goal or in the
+%  hypotheses.
 
-\item{\tt Pose {\term}}
+\item{\tt pose {\term}}
   
-  This behaves as {\tt Pose {\ident} := {\term}} but {\ident} is
-  generated by {\Coq}.
+  This behaves as {\tt pose (} {\ident} := {\term} {\tt )} but
+  {\ident} is generated by {\Coq}.
 
 \end{Variants}
 
-\subsection{\tt Assert {\ident} : {\form}}
-\tacindex{Assert}
+\subsection{{\tt assert ( {\ident} : {\form} \tt )}}
+\tacindex{assert}
 
-This tactic applies to any goal. {\tt Assert H : U} adds a new
+This tactic applies to any goal. {\tt assert (H : U)} adds a new
 hypothesis of name \texttt{H} asserting \texttt{U} to the current goal
 and opens a new subgoal \texttt{U}\footnote{This corresponds to the
   cut rule of sequent calculus.}. The subgoal {\texttt U} comes first
@@ -466,15 +425,15 @@ in the list of subgoals remaining to prove.
 \end{ErrMsgs}
 
 \begin{Variants}
-\item{\tt Assert {\form}}
+\item{\tt assert {\form}}
   
-  This behaves as {\tt Assert {\ident} : {\form}} but {\ident} is
-  generated by {\Coq}.
+  This behaves as {\tt assert (} {\ident} : {\form} {\tt )} but
+  {\ident} is generated by {\Coq}.
 
-\item{\tt Assert {\ident} := {\term}}
+\item{\tt assert (} {\ident} := {\term} {\tt )}
   
-  This behaves as {\tt Assert {\ident} : {\type};[exact
-    {\term}|Idtac]} where {\type} is the type of {\term}.
+  This behaves as {\tt assert ({\ident} : {\type});[exact
+    {\term}|idtac]} where {\type} is the type of {\term}.
 
 \item {\tt cut {\form}}\tacindex{cut} 
   
@@ -607,8 +566,8 @@ This tactic applies to any goal. It implements the rule
 \index[tactic]{Binding list}
 
 A bindings list is generally used after the keyword {\tt with} in
-tactics.  The general shape of a bindings list is {\tt \vref$_1$ :=
-  \term$_1$ \dots\ \vref$_n$ := \term$_n$} where {\vref} is either an
+tactics.  The general shape of a bindings list is {\tt (\vref$_1$ :=
+  \term$_1$) \dots\ (\vref$_n$ := \term$_n$)} where {\vref} is either an
 {\ident} or a {\num}. It is used to provide a tactic with a list of
 values (\term$_1$, \dots, \term$_n$) that have to be substituted
 respectively to \vref$_1$, \dots, \vref$_n$. For all $i \in [1\dots\ 
@@ -1862,7 +1821,7 @@ against the hints rather than pattern-matching
 As a consequence, {\tt eauto} can solve such a goal:
 
 \begin{coq_example}
-Hints Resolve ex_intro .
+Hints Resolve ex_intro.
 Goal forall P:nat -> Prop, P 0 ->  EX n : _ | P n.
 eauto.
 \end{coq_example}
@@ -1907,12 +1866,8 @@ The following goal can be proved by {\tt tauto} whereas {\tt auto}
 would fail:
 
 \begin{coq_example}
-Goal
-
-  forall (x:nat) (P:nat -> Prop), x = 0 \/ P x -> x <> 0 -> P x.
-
+Goal forall (x:nat) (P:nat -> Prop), x = 0 \/ P x -> x <> 0 -> P x.
   intros.
-
   tauto.
 \end{coq_example}
 \begin{coq_eval}
@@ -1924,10 +1879,8 @@ introductions. Therefore, the use of {\tt intros} in the previous
 proof is unnecessary. {\tt tauto} can for instance prove the
 following:
 \begin{coq_example}
-Goal
- (* auto would fail *)
-  
-  forall (A:Prop) (P:nat -> Prop),
+(* auto would fail *)
+Goal forall (A:Prop) (P:nat -> Prop),
     A \/ (forall x:nat, ~ A -> P x) -> forall x:nat, ~ A -> P x.
 
   tauto.
@@ -1939,9 +1892,7 @@ Abort.
 \Rem In contrast, {\tt tauto} cannot solve the following goal
 
 \begin{coq_example*}
-Goal
-
-  forall (A:Prop) (P:nat -> Prop),
+Goal forall (A:Prop) (P:nat -> Prop),
     A \/ (forall x:nat, ~ A -> P x) -> forall x:nat, ~ ~ (A \/ P x).
 \end{coq_example*}
 \begin{coq_eval}
@@ -1964,11 +1915,11 @@ original one (but simpler than it) and applies the tactic
 
 For instance, the tactic {\tt intuition auto} applied to the goal
 \begin{verbatim}
-((x:nat)(P x))/\B->((y:nat)(P y))/\(P O)\/B/\(P O)
+(forall (x:nat), P x)/\B -> (foral (y:nat),P y)/\ P O \/B/\ P O
 \end{verbatim}
 internally replaces it by the equivalent one:
 \begin{verbatim}
-(x:nat)(P x) ; B |- (P O)
+(forall (x:nat), P x), B |- P O
 \end{verbatim}
 and then uses {\tt auto} which completes the proof.
 
@@ -2153,7 +2104,7 @@ Variable f:A->A*A.
 \end{coq_eval}
 
 \begin{coq_example}
-Theorem inj : f=(pair a) -> (Some (f c)) = (Some (f d)) -> c=d.
+Theorem inj : f = pair a -> Some (f c) = Some (f d) -> c=d.
 intros.
 congruence.
 \end{coq_example}
@@ -2208,7 +2159,7 @@ normal form.
 
 \item \texttt{ring\_nat} is a tactic macro for \texttt{repeat rewrite
     S\_to\_plus\_one; ring}. The theorem \texttt{S\_to\_plus\_one} is a
-  proof that \texttt{(n:nat)(S n)=(plus (S O) n)}.
+  proof that \texttt{forall (n:nat), S n = plus (S O) n}.
 
 \end{Variants}
 
@@ -2220,8 +2171,7 @@ Open Scope Z_scope.
 \end{coq_eval}
 \begin{coq_example}
 Require Import ZArithRing.
-Goal
-forall a b c:Z,
+Goal forall a b c:Z,
   (a + b + c) * (a + b + c) =
   a * a + b * b + c * c + 2 * a * b + 2 * a * c + 2 * b * c.
 \end{coq_example}
@@ -2251,8 +2201,7 @@ the {\tt Add Field} command.
 \Example
 \begin{coq_example*}
 Require Import Reals.
-Goal
-  forall x y:R,
+Goal forall x y:R,
     (x * y > 0)%R ->
     (x * (1 / x + x / (x + y)))%R =
     ((- 1 / y) * y * (- x * (x / (x + y)) - 1))%R.
@@ -2654,117 +2603,6 @@ Conversely, when the user does \texttt{Require A.}, all hints
 of the module \texttt{A} that are not defined inside a section are
 loaded.
 
-\section{Tacticals}
-\index[tactic]{Tacticals}\index{Tacticals}\label{Tacticals}
-We describe in this section how to combine the tactics provided by the
-system to write synthetic proof scripts called {\em tacticals}. The
-tacticals are built using tactic operators we present below.
-
-\subsection{\tt idtac}
-\tacindex{idtac}
-\index{Tacticals!idtac@{\tt idtac}} The constant {\tt idtac} is the
-identity tactic: it leaves any goal unchanged.
-
-\subsection{\tt fail}
-\tacindex{fail}
-\index{Tacticals!fail@{\tt fail}}
-
-The tactic {\tt fail} is the always-failing tactic: it does not solve
-any goal. It is useful for defining other tacticals.
-
-\subsection{\tt do {\num} {\tac}}
-\tacindex{do}
-\index{Tacticals!do@{\tt do}}
-This tactic operator repeats {\num} times the tactic {\tac}. It fails
-when it is not possible to repeat {\num} times the tactic.
-
-\subsection{\tt \tac$_1$ {\tt ||} \tac$_2$}
-\tacindex{||}
-\index{Tacticals!orelse@{\tt ||}}
-The tactical \tac$_1$ {\tt ||} \tac$_2$ tries to apply \tac$_1$
-and, in case of a failure, applies \tac$_2$. It associates to the
-left.
-
-\subsection{\tt repeat {\tac}}
-\index[tactic]{repeat@{\tt repeat}}
-\index{Tacticals!repeat@{\tt repeat}}
-
-This tactic operator repeats {\tac} as long as it does not fail.
-
-\subsection{\tt {\tac}$_1$ {\tt ;} \tac$_2$}
-\index{;@{\tt ;}}
-\index[tactic]{;@{\tt ;}}
-\index{Tacticals!yy@{\tt {\tac$_1$};\tac$_2$}}
-This tactic operator is a generalized composition for sequencing.  The
-tactical {\tac}$_1$ {\tt ;} \tac$_2$ first applies \tac$_1$ and
-then applies \tac$_2$ to any
-subgoal generated by \tac$_1$. {\tt ;} associates to the left.
-
-\subsection{\tt \tac$_0$; [ \tac$_1$ | \dots\ | \tac$_n$ ]}
-\index[tactic]{;[]@{\tt ;[\ldots$\mid$\ldots$\mid$\ldots]}}
-\index{;[]@{\tt ;[\ldots$\mid$\ldots$\mid$\ldots]}}
-\index{Tacticals!zz@{\tt {\tac$_0$};[{\tac$_1$}$\mid$\ldots$\mid$\tac$_n$]}}
-
-This tactic operator is a generalization of the precedent tactics
-operator. The tactical {\tt \tac$_0$ ; [ \tac$_1$ | \dots\ | \tac$_n$ ]}
-first applies \tac$_0$ and then
-applies \tac$_i$ to the i-th subgoal generated by \tac$_0$. It  fails if
-$n$ is not the exact number of remaining subgoals.
-
-\subsection{\tt try {\tac}}
-\tacindex{try}
-\index{Tacticals!try@{\tt try}}
-This tactic operator applies tactic \tac, and catches the possible
-failure of \tac. It never fails.
-
-\subsection{\tt first [ \tac$_0$ | \dots\ | \tac$_n$ ]}
-\tacindex{first}
-\index{Tacticals!first@{\tt first}}
-
-This tactic operator tries to apply the tactics \tac$_i$ with $i=0\ldots{}n$,
-starting from $i=0$, until one of them does not fail. It fails if all the
-tactics fail.
-
-\begin{ErrMsgs}
-\item \errindex{No applicable tactic.}
-\end{ErrMsgs}
-
-\subsection{\tt solve [ \tac$_0$ | \dots\ | \tac$_n$ ]}
-\tacindex{solve}
-\index{Tacticals!solve@{\tt solve}}
-
-This tactic operator tries to solve the current goal with the tactics \tac$_i$
-with $i=0\ldots{}n$, starting from $i=0$, until one of them solves. It fails if
-no tactic can solve.
-
-\begin{ErrMsgs}
-\item \errindex{Cannot solve the goal.}
-\end{ErrMsgs}
-
-\subsection{\tt info {\tac}}
-\tacindex{info}
-\index{Tacticals!info@{\tt info}}
-This is not really a tactical. For elementary tactics, this is
-equivalent to \tac. For complex tactic like \texttt{auto}, it displays
-the operations performed by the tactic.
-
-\subsection{\tt abstract {\tac}}
-\tacindex{abstract}
-\index{Tacticals!abstract@{\tt abstract}}
-From outside, typing \texttt{abstract \tac} is the same that
-typing \tac. Internally it saves an auxiliary lemma called 
-{\ident}\texttt{\_subproof}\textit{n} where {\ident} is the name of the
-current goal and \textit{n} is chosen so that this is a fresh name.
-
-This tactical is useful with tactics such \texttt{Omega} or
-\texttt{discriminate} that generate big proof terms. With that tool
-the user can avoid the explosion at time of the \texttt{Save} command
-without having to cut ``by hand'' the proof in smaller lemmas.
-
-\begin{Variants}
-\item \texttt{abstract {\tac} using {\ident}}.\\
-  Give explicitly the name of the auxiliary lemma.
-\end{Variants}
 
 \section{Generation of induction principles with {\tt Scheme}}
 \label{Scheme}
diff --git a/doc/RefMan-tacex.tex b/doc/RefMan-tacex.tex
index 57b779281f..f82416869d 100644
--- a/doc/RefMan-tacex.tex
+++ b/doc/RefMan-tacex.tex
@@ -809,9 +809,407 @@ is undecidable in general case, don't expect miracles from it!
 
 \SeeAlso comments of source file \texttt{tactics/contrib/polynom/quote.ml}
 
-\SeeAlso the tactic \texttt{ring} (chapter \ref{ring})
+\SeeAlso the tactic \texttt{Ring} (chapter \ref{Ring})
 
 
+\section{Using the tactical language}
+
+\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{coq_eval}
+Reset Initial.
+Require Import Arith.
+Require Import List.
+\end{coq_eval}
+
+\begin{table}[ht]
+\noindent{}\framebox[6.4in][l]
+{\parbox{6.4in}
+{
+\begin{coq_example*}
+Lemma card_nat :
+ ~ (exists x : nat, exists y : nat, forall z:nat, x = z \/ y = z).
+Proof.
+red; intros (x, (y, Hy)).
+elim (Hy 0); elim (Hy 1); elim (Hy 2); intros;
+ match goal with
+ | [_:(?a = ?b),_:(?a = ?c) |- _ ] =>
+     cut (b = c); [ discriminate | apply trans_equal with a; auto ]
+ end.
+Qed.
+\end{coq_example*}
+}}
+\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 {\tt match goal} structure and, in particular, with only one pattern (use
+of non-linear matching).
+
+\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[6.4in][l]
+{\parbox{6.4in}
+{
+\begin{coq_example*}
+Section Sort.
+Variable A : Set.
+Inductive permut : list A -> list A -> Prop :=
+  | permut_refl   : forall l, permut l l
+  | permut_cons   :
+      forall a l0 l1, permut l0 l1 -> permut (a :: l0) (a :: l1)
+  | permut_append : forall a l, permut (a :: l) (l ++ a :: nil)
+  | permut_trans  :
+      forall l0 l1 l2, permut l0 l1 -> permut l1 l2 -> permut l0 l2.
+End Sort.
+\end{coq_example*}
+}}
+\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 {\tt
+PermutProve} and {\tt Permut}. The function to be called is {\tt PermutProve}
+which computes the lengths of the two lists and calls {\tt Permut} with the
+length if the two lists have the same length. {\tt Permut} works as expected.
+If the two lists are equal, it concludes. Otherwise, if the lists have
+identical first elements, it applies {\tt 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 {\tt 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 {\tt 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 {\tt eval
+compute in} and we can get the terms back by {\tt match}.
+ 
+\begin{table}[p]
+\noindent{}\framebox[6.4in][l]
+{\parbox{6.4in}
+{
+\begin{coq_example}
+Ltac Permut n :=
+  match goal with
+  | |- (permut _ ?l ?l) => apply permut_refl
+  | |- (permut _ (?a :: ?l1) (?a :: ?l2)) =>
+      let newn := eval compute in (length l1) in
+      (apply permut_cons; Permut newn)
+  | |- (permut ?A (?a :: ?l1) ?l2) =>
+      match eval compute in n with
+      | 1 => fail
+      | _ =>
+          let l1' := constr:(l1 ++ a :: nil) in
+          (apply (permut_trans A (a :: l1) l1' l2);
+            [ apply permut_append | compute; Permut (pred n) ])
+      end
+  end.
+Ltac PermutProve :=
+  match goal with
+  | |- (permut _ ?l1 ?l2) =>
+      match eval compute in (length l1 = length l2) with
+      | (?n = ?n) => Permut n
+      end
+  end.
+\end{coq_example}
+}}
+\caption{Permutation tactic}
+\label{permutltac}
+\end{table}
+
+With {\tt PermutProve}, we can now prove lemmas such those shown in
+table~\ref{permutlem}.
+
+\begin{table}[p]
+\noindent{}\framebox[6.4in][l]
+{\parbox{6.4in}
+{
+\begin{coq_example*}
+Lemma permut_ex1 :
+  permut nat (1 :: 2 :: 3 :: nil) (3 :: 2 :: 1 :: nil).
+Proof.
+PermutProve.
+Qed.
+
+Lemma permut_ex2 :
+  permut nat
+    (0 :: 1 :: 2 :: 3 :: 4 :: 5 :: 6 :: 7 :: 8 :: 9 :: nil)
+    (0 :: 2 :: 4 :: 6 :: 8 :: 9 :: 7 :: 5 :: 3 :: 1 :: nil).
+Proof.
+PermutProve.
+Qed.
+\end{coq_example*}
+}}
+\caption{Examples of {\tt PermutProve} use}
+\label{permutlem}
+\end{table}
+
+\subsection{Deciding intuitionistic propositional logic}
+
+The pattern matching on goals allows a complete and so a powerful
+backtracking when returning tactic values. An interesting application
+is the problem of deciding intuitionistic propositional
+logic. Considering the contraction-free sequent calculi {\tt 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 {\tt Axioms} tries to conclude using usual axioms. The tactic
+{\tt DSimplif} applies all the reversible rules of Dyckhoff's
+system. Finally, the tactic {\tt TautoProp} (the main tactic to be
+called) simplifies with {\tt DSimplif}, tries to conclude with {\tt
+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[6.4in][l]
+{\parbox{6.4in}
+{
+\begin{coq_example}
+Ltac Axioms :=
+  match goal with
+  | |- True => trivial
+  | _:False |- _  => elimtype False; assumption
+  | _:?A |- ?A  => auto
+  end.
+Ltac DSimplif :=
+  repeat
+   (intros;
+    match goal with
+     | id:(~ _) |- _ => red in id
+     | id:(_ /\ _) |- _ =>
+         elim id; do 2 intro; clear id
+     | id:(_ \/ _) |- _ =>
+         elim id; intro; clear id
+     | id:(?A /\ ?B -> ?C) |- _ =>
+         cut (A -> B -> C);
+          [ intro | intros; apply id; split; assumption ]
+     | id:(?A \/ ?B -> ?C) |- _ =>
+         cut (B -> C);
+          [ cut (A -> C);
+             [ intros; clear id
+             | intro; apply id; left; assumption ]
+          | intro; apply id; right; assumption ]
+     | id0:(?A -> ?B),id1:?A |- _ =>
+         cut B; [ intro; clear id0 | apply id0; assumption ]
+     | |- (_ /\ _) => split
+     | |- (~ _) => red
+     end).
+Ltac TautoProp :=
+  DSimplif;
+   Axioms ||
+     match goal with
+     | id:((?A -> ?B) -> ?C) |- _ =>
+          cut (B -> C);
+          [ intro; cut (A -> B);
+             [ intro; cut C;
+                [ intro; clear id | apply id; assumption ]
+             | clear id ]
+          | intro; apply id; intro; assumption ]; TautoProp
+     | id:(~ ?A -> ?B) |- _ =>
+         cut (False -> B);
+          [ intro; cut (A -> False);
+             [ intro; cut B;
+                [ intro; clear id | apply id; assumption ]
+             | clear id ]
+          | intro; apply id; red; intro; assumption ]; TautoProp
+     | |- (_ \/ _) => (left; TautoProp) || (right; TautoProp)
+     end.
+\end{coq_example}
+}}
+\caption{Deciding intuitionistic propositions}
+\label{tautoltac}
+\end{table}
+
+For example, with {\tt TautoProp}, we can prove tautologies like those in
+table~\ref{tautolem}.
+
+\begin{table}[ht]
+\noindent{}\framebox[6.4in][l]
+{\parbox{6.4in}
+{
+\begin{coq_example*}
+Lemma tauto_ex1 : forall A B:Prop, A /\ B -> A \/ B.
+Proof.
+TautoProp.
+Qed.
+
+Lemma tauto_ex2 :
+   forall A B:Prop, (~ ~ B -> B) -> (A -> B) -> ~ ~ A -> B.
+Proof.
+TautoProp.
+Qed.
+\end{coq_example*}
+}}
+\caption{Proofs of tautologies with {\tt 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[6.4in][l]
+{\parbox{6.4in}
+{
+\begin{coq_eval}
+Reset Initial.
+\end{coq_eval}
+\begin{coq_example*}
+Open Scope type_scope.
+Section Iso_axioms.
+Variables A B C : Set.
+Axiom Com : A * B = B * A.
+Axiom Ass : A * (B * C) = A * B * C.
+Axiom Cur : (A * B -> C) = (A -> B -> C).
+Axiom Dis : (A -> B * C) = (A -> B) * (A -> C).
+Axiom P_unit : A * unit = A.
+Axiom AR_unit : (A -> unit) = unit.
+Axiom AL_unit : (unit -> A) = A.
+Lemma Cons : B = C -> A * B = A * C.
+Proof.
+intro Heq; rewrite Heq; apply refl_equal.
+Qed.
+End Iso_axioms.
+\end{coq_example*}
+}}
+\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 {\tt
+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 {\tt
+CompareStruct}). The main tactic to be called and realizing this algorithm is
+{\tt IsoProve}.
+
+\begin{table}[ht]
+\noindent{}\framebox[6.4in][l]
+{\parbox{6.4in}
+{
+\begin{coq_example}
+Ltac DSimplif trm :=
+  match trm with
+  | (?A * ?B * ?C) =>
+      rewrite <- (Ass A B C); try MainSimplif
+  | (?A * ?B -> ?C) =>
+      rewrite (Cur A B C); try MainSimplif
+  | (?A -> ?B * ?C) =>
+      rewrite (Dis A B C); try MainSimplif
+  | (?A * unit) =>
+      rewrite (P_unit A); try MainSimplif
+  | (unit * ?B) =>
+      rewrite (Com unit B); try MainSimplif
+  | (?A -> unit) =>
+      rewrite (AR_unit A); try MainSimplif
+  | (unit -> ?B) =>
+      rewrite (AL_unit B); try MainSimplif
+  | (?A * ?B) =>
+      (DSimplif A; try MainSimplif) || (DSimplif B; try MainSimplif)
+  | (?A -> ?B) =>
+      (DSimplif A; try MainSimplif) || (DSimplif B; try MainSimplif)
+  end
+ with MainSimplif :=
+  match goal with
+  | |- (?A = ?B) => try DSimplif A; try DSimplif B
+  end.
+Ltac Length trm :=
+  match trm with
+  | (_ * ?B) => let succ := Length B in constr:(S succ)
+  | _ => constr:1
+  end.
+Ltac assoc := repeat rewrite <- Ass.
+\end{coq_example}
+}}
+\caption{Type isomorphism tactic (1)}
+\label{isosltac1}
+\end{table}
+
+\begin{table}[ht]
+\noindent{}\framebox[6.4in][l]
+{\parbox{6.4in}
+{
+\begin{coq_example}
+Ltac DoCompare n :=
+  match goal with
+  | [ |- (?A = ?A) ] => apply refl_equal
+  | [ |- (?A * ?B = ?A * ?C) ] =>
+      apply Cons; let newn := Length B in
+                  DoCompare newn
+  | [ |- (?A * ?B = ?C) ] =>
+      match eval compute in n with
+      | 1 => fail
+      | _ =>
+          pattern (A * B) at 1; rewrite Com; assoc; DoCompare (pred n)
+      end
+  end.
+Ltac CompareStruct :=
+  match goal with
+  | [ |- (?A = ?B) ] =>
+      let l1 := Length A
+      with l2 := Length B in
+      match eval compute in (l1 = l2) with
+      | (?n = ?n) => DoCompare n
+      end
+  end.
+Ltac IsoProve := MainSimplif; CompareStruct.
+\end{coq_example}
+}}
+\caption{Type isomorphism tactic (2)}
+\label{isosltac2}
+\end{table}
+
+Table~\ref{isoslem} gives examples of what can be solved by {\tt IsoProve}.
+
+\begin{table}[ht]
+\noindent{}\framebox[6.4in][l]
+{\parbox{6.4in}
+{
+\begin{coq_example*}
+Lemma isos_ex1 : 
+  forall A B:Set, A * unit * B = B * (unit * A).
+Proof.
+intros; IsoProve.
+Qed.
+
+Lemma isos_ex2 :
+  forall A B C:Set,
+    (A * unit -> B * (C * unit)) =
+    (A * unit -> (C -> unit) * C) * (unit -> A -> B).
+Proof.
+intros; IsoProve.
+Qed.
+\end{coq_example*}
+}}
+\caption{Type equalities solved by {\tt IsoProve}}
+\label{isoslem}
+\end{table}
+
 %%% Local Variables: 
 %%% mode: latex
 %%% TeX-master: "Reference-Manual"
diff --git a/doc/RefMan.txt b/doc/RefMan.txt
index 61afe8bd7f..b2ce8a1395 100644
--- a/doc/RefMan.txt
+++ b/doc/RefMan.txt
@@ -29,7 +29,7 @@ MANUEL DE REFERENCE
 \include{RefMan-syn.v}% The Syntax and the Grammar commands	HH
 %%SUPPRIME \include{RefMan-tus.v}% Writing tactics
 %%REMPLACE PAR
-\include{RefMan-ltac.v}% Writing tactics			BB
+\include{RefMan-ltac.v}% Writing tactics			BB -fait
 
 \part{Practical tools}
 \include{RefMan-com}% The coq commands (coqc coqtop)		HH
diff --git a/doc/macros.tex b/doc/macros.tex
index d85a9601e3..50ced80e85 100755
--- a/doc/macros.tex
+++ b/doc/macros.tex
@@ -89,14 +89,19 @@
 
 \newcommand{\nterm}[1]{\textrm{\textsl{#1}}}
 
+\newcommand{\qstring}{\nterm{string}}
+
 %% New syntax specific entries
-\newcommand{\termarg}{\nterm{arg}}
+\newcommand{\annotation}{\nterm{annotation}}
+\newcommand{\binder}{\nterm{binder}}
+\newcommand{\binderlist}{\nterm{binderlist}}
 \newcommand{\caseitems}{\nterm{caseitems}}
 \newcommand{\caseitem}{\nterm{case\_item}}
 \newcommand{\casetype}{\nterm{casetype}}
+\newcommand{\eqn}{\nterm{equation}}
 \newcommand{\letclauses}{\nterm{letclauses}}
-\newcommand{\annotation}{\nterm{annotation}}
 \newcommand{\returntype}{\nterm{return\_type}}
+\newcommand{\termarg}{\nterm{arg}}
 
 \newcommand{\typecstr}{\zeroone{{\tt :} {\term}}}
 
@@ -104,9 +109,6 @@
 \newcommand{\Index}{\textrm{\textsl{index}}}
 \newcommand{\abbrev}{\textrm{\textsl{abbreviation}}}
 \newcommand{\atomictac}{\textrm{\textsl{atomic\_tactic}}}
-\newcommand{\binders}{\textrm{\textsl{bindings}}}
-\newcommand{\binder}{\textrm{\textsl{binding}}}
-\newcommand{\binderlist}{\nterm{binderlist}}
 \newcommand{\bindinglist}{\textrm{\textsl{bindings\_list}}}
 \newcommand{\cast}{\textrm{\textsl{cast}}}
 \newcommand{\cofixpointbodies}{\textrm{\textsl{cofix\_bodies}}}
@@ -118,7 +120,6 @@
 \newcommand{\declaration}{\textrm{\textsl{declaration}}}
 \newcommand{\definition}{\textrm{\textsl{definition}}}
 \newcommand{\digit}{\textrm{\textsl{digit}}}
-\newcommand{\eqn}{\textrm{\textsl{equation}}}
 \newcommand{\exteqn}{\textrm{\textsl{ext\_eqn}}}
 \newcommand{\field}{\textrm{\textsl{field}}}
 \newcommand{\firstletter}{\textrm{\textsl{first\_letter}}}