- Fixed various Overfull in documentation.

- Removed useless coq-tex preprocessing of RecTutorial.
- Make "Set Printing Width" applies to "Show Script" too.
- Completed documentation (specially of ltac) according to CHANGES file.



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

9 files changed, 131 insertions, 88 deletions

diff --git a/Makefile.doc b/Makefile.doc
index 5afd12393..9382e1b6f 100644
--- a/Makefile.doc
+++ b/Makefile.doc
@@ -17,15 +17,15 @@ doc: refman faq tutorial rectutorial stdlib ide/index_urls.txt
 
 doc-html:\
   doc/tutorial/Tutorial.v.html doc/refman/html/index.html \
-  doc/faq/html/index.html doc/stdlib/html/index.html doc/RecTutorial/RecTutorial.v.html
+  doc/faq/html/index.html doc/stdlib/html/index.html doc/RecTutorial/RecTutorial.html
 
 doc-pdf:\
   doc/tutorial/Tutorial.v.pdf doc/refman/Reference-Manual.pdf \
-  doc/faq/FAQ.v.pdf doc/stdlib/Library.pdf doc/RecTutorial/RecTutorial.v.pdf
+  doc/faq/FAQ.v.pdf doc/stdlib/Library.pdf doc/RecTutorial/RecTutorial.pdf
 
 doc-ps:\
   doc/tutorial/Tutorial.v.ps doc/refman/Reference-Manual.ps \
-  doc/faq/FAQ.v.ps doc/stdlib/Library.ps doc/RecTutorial/RecTutorial.v.ps
+  doc/faq/FAQ.v.ps doc/stdlib/Library.ps doc/RecTutorial/RecTutorial.ps
 
 refman: \
   doc/refman/html/index.html doc/refman/Reference-Manual.ps doc/refman/Reference-Manual.pdf
@@ -38,8 +38,8 @@ stdlib: \
 
 faq: doc/faq/html/index.html doc/faq/FAQ.v.ps doc/faq/FAQ.v.pdf
 
-rectutorial: doc/RecTutorial/RecTutorial.v.html \
-  doc/RecTutorial/RecTutorial.v.ps doc/RecTutorial/RecTutorial.v.pdf
+rectutorial: doc/RecTutorial/RecTutorial.html \
+  doc/RecTutorial/RecTutorial.ps doc/RecTutorial/RecTutorial.pdf
 
 ######################################################################
 ### Implicit rules
@@ -216,32 +216,32 @@ doc/stdlib/Library.dvi: $(DOCCOMMON) doc/stdlib/Library.coqdoc.tex doc/stdlib/Li
 	(cd doc/stdlib;\
 	$(LATEX) -interaction=batchmode Library;\
 	$(LATEX) -interaction=batchmode Library > /dev/null;\
-	../tools/show_latex_messages Library.log)
+	../tools/show_latex_messages -no-overfull Library.log)
 
 doc/stdlib/Library.pdf: $(DOCCOMMON) doc/stdlib/Library.coqdoc.tex doc/stdlib/Library.dvi
 	(cd doc/stdlib;\
 	$(PDFLATEX) -interaction=batchmode Library;\
-	../tools/show_latex_messages Library.log)
+	../tools/show_latex_messages -no-overfull Library.log)
 
 ######################################################################
 # Tutorial on inductive types
 ######################################################################
 
-doc/RecTutorial/RecTutorial.v.dvi: doc/common/version.tex doc/common/title.tex doc/RecTutorial/RecTutorial.v.tex
+doc/RecTutorial/RecTutorial.dvi: doc/common/version.tex doc/common/title.tex doc/RecTutorial/RecTutorial.tex
 	(cd doc/RecTutorial;\
-	$(LATEX) -interaction=batchmode RecTutorial.v;\
-	$(BIBTEX) -terse RecTutorial.v;\
-	$(LATEX) -interaction=batchmode RecTutorial.v > /dev/null;\
-	$(LATEX) -interaction=batchmode RecTutorial.v > /dev/null;\
-	../tools/show_latex_messages RecTutorial.v.log)
+	$(LATEX) -interaction=batchmode RecTutorial;\
+	$(BIBTEX) -terse RecTutorial;\
+	$(LATEX) -interaction=batchmode RecTutorial > /dev/null;\
+	$(LATEX) -interaction=batchmode RecTutorial > /dev/null;\
+	../tools/show_latex_messages RecTutorial.log)
 
-doc/RecTutorial/RecTutorial.v.pdf: doc/common/version.tex doc/common/title.tex doc/RecTutorial/RecTutorial.v.dvi
+doc/RecTutorial/RecTutorial.pdf: doc/common/version.tex doc/common/title.tex doc/RecTutorial/RecTutorial.dvi
 	(cd doc/RecTutorial;\
-	$(PDFLATEX) -interaction=batchmode RecTutorial.v.tex;\
-	../tools/show_latex_messages RecTutorial.v.log)
+	$(PDFLATEX) -interaction=batchmode RecTutorial.tex;\
+	../tools/show_latex_messages RecTutorial.log)
 
-doc/RecTutorial/RecTutorial.v.html: doc/RecTutorial/RecTutorial.v.tex
-	(cd doc/RecTutorial; $(HEVEA) $(HEVEAOPTS) RecTutorial.v)
+doc/RecTutorial/RecTutorial.html: doc/RecTutorial/RecTutorial.tex
+	(cd doc/RecTutorial; $(HEVEA) $(HEVEAOPTS) RecTutorial)
 
 ######################################################################
 # Index file for CoqIDE
@@ -267,7 +267,7 @@ install-doc-html:
 	$(MKDIR) $(addprefix $(FULLDOCDIR)/html/, refman stdlib faq)
 	$(INSTALLLIB) doc/refman/html/* $(FULLDOCDIR)/html/refman 
 	$(INSTALLLIB) doc/stdlib/html/* $(FULLDOCDIR)/html/stdlib 
-	$(INSTALLLIB) doc/RecTutorial/RecTutorial.v.html $(FULLDOCDIR)/html/RecTutorial.html
+	$(INSTALLLIB) doc/RecTutorial/RecTutorial.html $(FULLDOCDIR)/html/RecTutorial.html
 	$(INSTALLLIB) doc/faq/html/* $(FULLDOCDIR)/html/faq
 	$(INSTALLLIB) doc/tutorial/Tutorial.v.html $(FULLDOCDIR)/html/Tutorial.html
 
@@ -278,8 +278,8 @@ install-doc-printable:
 	$(INSTALLLIB) doc/refman/Reference-Manual.ps \
 		doc/stdlib/Library.ps $(FULLDOCDIR)/ps
 	$(INSTALLLIB) doc/tutorial/Tutorial.v.pdf $(FULLDOCDIR)/pdf/Tutorial.pdf
-	$(INSTALLLIB) doc/RecTutorial/RecTutorial.v.pdf $(FULLDOCDIR)/pdf/RecTutorial.pdf
+	$(INSTALLLIB) doc/RecTutorial/RecTutorial.pdf $(FULLDOCDIR)/pdf/RecTutorial.pdf
 	$(INSTALLLIB) doc/faq/FAQ.v.pdf $(FULLDOCDIR)/pdf/FAQ.pdf
 	$(INSTALLLIB) doc/tutorial/Tutorial.v.ps $(FULLDOCDIR)/ps/Tutorial.ps
-	$(INSTALLLIB) doc/RecTutorial/RecTutorial.v.ps $(FULLDOCDIR)/ps/RecTutorial.ps
+	$(INSTALLLIB) doc/RecTutorial/RecTutorial.ps $(FULLDOCDIR)/ps/RecTutorial.ps
 	$(INSTALLLIB) doc/faq/FAQ.v.ps $(FULLDOCDIR)/ps/FAQ.ps
diff --git a/doc/RecTutorial/RecTutorial.tex b/doc/RecTutorial/RecTutorial.tex
index 79b4f7f1a..372f13326 100644
--- a/doc/RecTutorial/RecTutorial.tex
+++ b/doc/RecTutorial/RecTutorial.tex
@@ -724,7 +724,7 @@ for \linebreak ``~\citecoq{ex (fun $x$:$A$ \funarrow{} $B$)}~''.
 \noindent The former quantifier inhabits the universe of propositions.
 As for the conjunction and disjunction connectives, there is also another
 version of existential quantification inhabiting the universes $\Type_i$,
-which is noted \texttt{sig $P$}. The syntax
+which is written \texttt{sig $P$}. The syntax
 ``~\citecoq{\{$x$:$A$ | $B$\}}~'' is an abreviation for ``~\citecoq{sig (fun $x$:$A$ {\funarrow} $B$)}~''.
 
 
@@ -934,7 +934,7 @@ Definition  predecessor : {\prodsym} n:nat, pred_spec n.
 Defined.
 \end{alltt}
 
-If we print the term built by {\coq}, we can observe its dependent pattern-matching structure:
+If we print the term built by {\coq}, its dependent pattern-matching structure can be observed:
 
 \begin{alltt}
 predecessor =  fun n : nat {\funarrow}
@@ -950,8 +950,9 @@ predecessor =  fun n : nat {\funarrow}
 \end{alltt}
 
 
-Notice that there are many variants to the pattern ``~\texttt{intros \dots; case \dots}~''. Look at the reference manual and/or the book: tactics
-\texttt{destruct}, ``~\texttt{intro \emph{pattern}}~'', etc.
+Notice that there are many variants to the pattern ``~\texttt{intros \dots; case \dots}~''. Look at for tactics
+``~\texttt{destruct}~'', ``~\texttt{intro \emph{pattern}}~'', etc. in 
+the reference manual and/or the book. 
 
 \noindent The command \texttt{Extraction} \refmancite{Section
 \ref{ExtractionIdent}} can be used to see the computational
@@ -1240,7 +1241,7 @@ Let $n$ and $p$ be terms of type \citecoq{nat}, and $Q$ a predicate
 of type $\citecoq{nat}\arrow{}\Prop$.
 If $H$ is a proof of ``~\texttt{n {\coqle} p}~'',
 $H_0$ a proof of ``~\texttt{$Q$  n}~'' and
-$H_S$ a proof of ``~\citecoq{{\prodsym}m:nat, n {\coqle}  m {\arrow} Q (S m)}~'',
+$H_S$ a proof of the statement ``~\citecoq{{\prodsym}m:nat, n {\coqle}  m {\arrow} Q (S m)}~'',
 then the term
 \begin{alltt}
 match H in (_ {\coqle} q) return (Q q) with
@@ -2604,8 +2605,8 @@ End Principle_of_Double_Induction.
 \end{alltt}
 
 Changing the type of $P$ into $\nat\rightarrow\nat\rightarrow\Type$,
-another combinator \texttt{nat\_double\_rect} for constructing 
-(certified) programs can be defined in exactly the same way.
+another combinator for constructing 
+(certified) programs, \texttt{nat\_double\_rect}, can be defined in exactly the same way.
 This definition is left as an exercise.\label{natdoublerect}
 
 \iffalse
@@ -2751,8 +2752,8 @@ has a universally quantified formula as conclusion, which confuses
 
 
 Therefore,
-in this case the abstraction must be explicited using the tactic
-\texttt{pattern}. Once the right abstraction is provided, the rest of
+in this case the abstraction must be explicited using the 
+\texttt{pattern} tactic. Once the right abstraction is provided, the rest of
 the proof is immediate:
 
 \begin{alltt}
@@ -2804,8 +2805,8 @@ Defined.
 
 \begin{exercise}
 \begin{enumerate}
-\item Define a recursive  function \emph{nat2itree}
-mapping any natural number $n$ into an infinitely branching
+\item Define a recursive  function of name \emph{nat2itree}
+that maps any natural number $n$ into an infinitely branching
 tree of height $n$.
 \item Provide an elimination combinator for these trees.
 \item Prove that the relation \citecoq{itree\_le} is a preorder 
@@ -2831,7 +2832,7 @@ for all n and p. (\citecoq{le'} is defined in section \ref{parameterstuff}).
 
 Structural induction is a strong elimination rule for inductive types.
 This method can be used to define any function whose termination is
-based on the well-foundedness of certain order relation $R$ decreasing
+a consequence of the well-foundedness of a certain order relation $R$ decreasing
 at each recursive call. What makes this principle so strong is the
 possibility of reasoning by structural induction on the proof that
 certain $R$ is well-founded.  In order to illustrate this we have
@@ -2867,8 +2868,8 @@ let rec div x y =
 \end{verbatim}
 
 
-The equality test on natural numbers can be represented as the
-function \textsl{eq\_nat\_dec} defined page \pageref{iseqpage}. Giving $x$ and
+The equality test on natural numbers can be implemented using the
+function \textsl{eq\_nat\_dec} that is defined page \pageref{iseqpage}. Giving $x$ and
 $y$, this function yields either the value $(\textsl{left}\;p)$ if
 there exists a proof $p:x=y$, or the value $(\textsl{right}\;q)$ if
 there exists $q:a\not = b$. The subtraction function is already
@@ -3112,7 +3113,7 @@ The term "Vnil A" has type "vector A 0" while it is expected to have type
  "vector A n"
 \end{alltt}
 
-In effect, the equality ``~\citecoq{v = Vnil A}~'' is ill typed,
+In effect, the equality ``~\citecoq{v = Vnil A}~'' is ill-typed and this is
 because the type ``~\citecoq{vector A n}~'' is not \emph{convertible}
 with ``~\citecoq{vector A 0}~''.
 
@@ -3264,11 +3265,11 @@ on vectors of same length:
 
 \begin{alltt}
 Definition vector_double_rect : 
-    {\prodsym} (A:Type) (P: {\prodsym} (n:nat),(vector A n){\arrow}(vector A n) {\arrow} Type),
-        P 0 Vnil Vnil {\arrow}
-        ({\prodsym} n (v1 v2 : vector A n) a b, P n v1 v2 {\arrow}
-             P (S n) (Vcons a v1) (Vcons  b v2)) {\arrow}
-        {\prodsym} n (v1 v2 : vector A n), P n v1 v2.
+ {\prodsym} (A:Type) (P: {\prodsym} (n:nat),(vector A n){\arrow}(vector A n) {\arrow} Type),
+     P 0 Vnil Vnil {\arrow}
+     ({\prodsym} n (v1 v2 : vector A n) a b, P n v1 v2 {\arrow}
+          P (S n) (Vcons a v1) (Vcons  b v2)) {\arrow}
+     {\prodsym} n (v1 v2 : vector A n), P n v1 v2.
  induction n.
  intros; rewrite (zero_nil _ v1); rewrite (zero_nil _ v2).
  auto.
@@ -3361,7 +3362,7 @@ CoInductive LList (A: Type) : Type :=
 
 
 It is also possible to define  co-inductive types for the 
-trees with infinite branches (see Chapter 13 of~\cite{coqart}).
+trees with infinitely-many branches (see Chapter 13 of~\cite{coqart}).
 
 Structural induction is the way of expressing that inductive types
 only contain well-founded objects. Hence, this elimination principle
@@ -3555,7 +3556,7 @@ Qed.
 \end{alltt}
 
 \begin{exercise}
-Define a co-inductive type $Nat$ containing non-standard 
+Define a co-inductive type of name $Nat$ that contains non-standard 
 natural numbers --this is, verifying 
 
 $$\exists m  \in \mbox{\texttt{Nat}}, \forall\, n \in \mbox{\texttt{Nat}}, n<m$$.
@@ -3591,8 +3592,8 @@ Proof.
 Qed.
 
 Lemma injection_demo : {\prodsym} (A:Type)(a b : A)(l l': LList A),
-                       LCons a (LCons b l) = LCons b (LCons a l') {\arrow}
-                       a = b {\coqand} l = l'.
+                  LCons a (LCons b l) = LCons b (LCons a l') {\arrow}
+                  a = b {\coqand} l = l'.
 Proof.
  intros A a b l l' e; injection e; auto.
 Qed.
diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex
index 8b404f4ef..501f9b0b1 100644
--- a/doc/refman/RefMan-ext.tex
+++ b/doc/refman/RefMan-ext.tex
@@ -343,7 +343,7 @@ for all the arguments. For example, the preceding example can be written:
 Reset fst.
 \end{coq_eval}
 \begin{coq_example}
-Definition fst (A B:Set) (p:A * B) := let 'pair x _ := p in x.
+Definition fst (A B:Set) (p:A*B) := let 'pair x _ := p in x.
 \end{coq_example}
 
 This is useful to match deeper inside tuples and also to use notations
@@ -351,10 +351,10 @@ for the pattern, as the syntax {\tt let 'p := t in b} allows arbitrary
 patterns to do the deconstruction. For example:
 
 \begin{coq_example}
-Definition deep_tuple (A : Set) (x : (A * A) * (A * A)) : A * A * A * A :=
+Definition deep_tuple (A:Set) (x:(A*A)*(A*A)) : A*A*A*A :=
   let '((a,b), (c, d)) := x in (a,b,c,d).
 Notation " x 'with' p " := (exist _ x p) (at level 20).
-Definition proj1_sig' (A :Set) (P : A -> Prop) (t:{ x : A | P x }) : A :=
+Definition proj1_sig' (A:Set) (P:A->Prop) (t:{ x:A | P x }) : A :=
   let 'x with p := t in x.
 \end{coq_example}
 
diff --git a/doc/refman/RefMan-gal.tex b/doc/refman/RefMan-gal.tex
index 3a4d7f03e..48c18e265 100644
--- a/doc/refman/RefMan-gal.tex
+++ b/doc/refman/RefMan-gal.tex
@@ -226,7 +226,7 @@ Chapter \ref{Addoc-syntax}.
 
 \begin{figure}[htbp]
 \begin{centerframe}
-\begin{tabular}{lcl@{\qquad}r}
+\begin{tabular}{lcl@{\quad~}r}  % warning: page width exceeded with \qquad 
 {\term} & ::= &
          {\tt forall} {\binderlist} {\tt ,} {\term}  &(\ref{products})\\
  & $|$ & {\tt fun} {\binderlist} {\tt =>} {\term} &(\ref{abstractions})\\
@@ -266,10 +266,10 @@ Chapter \ref{Addoc-syntax}.
 {\binderlist} & ::= & \nelist{\name}{} {\typecstr} & \ref{Binders} \\
  & $|$ & {\binder} \nelist{\binderlet}{} &\\
 &&&\\
-{\binder} & ::= &   {\name} & \ref{Binders} \\
+{\binder} & ::= &   {\name} & (\ref{Binders}) \\
  & $|$ & {\tt (} \nelist{\name}{} {\tt :} {\term} {\tt )} &\\  
 &&&\\
-{\binderlet} & ::= & {\binder} & \ref{Binders} \\
+{\binderlet} & ::= & {\binder} & (\ref{Binders}) \\
  & $|$ & {\tt (} {\name} {\typecstr} {\tt :=} {\term} {\tt )} &\\
 & & &\\
 {\name} & ::= & {\ident} &\\
diff --git a/doc/refman/RefMan-lib.tex b/doc/refman/RefMan-lib.tex
index d15859047..24eb3d112 100644
--- a/doc/refman/RefMan-lib.tex
+++ b/doc/refman/RefMan-lib.tex
@@ -267,11 +267,11 @@ Abort.
 \begin{coq_example*}
 End equality.
 Definition eq_ind_r :
-  forall (A:Type) (x:A) (P:A -> Prop), P x -> forall y:A, y = x -> P y.
+  forall (A:Type) (x:A) (P:A->Prop), P x -> forall y:A, y = x -> P y.
 Definition eq_rec_r :
-  forall (A:Type) (x:A) (P:A -> Set), P x -> forall y:A, y = x -> P y.
+  forall (A:Type) (x:A) (P:A->Set), P x -> forall y:A, y = x -> P y.
 Definition eq_rect_r :
-  forall (A:Type) (x:A) (P:A -> Type), P x -> forall y:A, y = x -> P y.
+  forall (A:Type) (x:A) (P:A->Type), P x -> forall y:A, y = x -> P y.
 \end{coq_example*}
 \begin{coq_eval}
 Abort.
@@ -290,8 +290,9 @@ arguments. The theorem are names {\tt f\_equal2}, {\tt f\_equal3},
 For instance {\tt f\_equal3} is defined the following way.
 \begin{coq_example*}
 Theorem f_equal3 :
- forall (A1 A2 A3 B:Type) (f:A1 -> A2 -> A3 -> B) (x1 y1:A1) (x2 y2:A2)
-   (x3 y3:A3), x1 = y1 -> x2 = y2 -> x3 = y3 -> f x1 x2 x3 = f y1 y2 y3.
+ forall (A1 A2 A3 B:Type) (f:A1 -> A2 -> A3 -> B)
+   (x1 y1:A1) (x2 y2:A2) (x3 y3:A3),
+   x1 = y1 -> x2 = y2 -> x3 = y3 -> f x1 x2 x3 = f y1 y2 y3.
 \end{coq_example*}
 \begin{coq_eval}
 Abort.
@@ -478,7 +479,9 @@ in the \verb"Set" \verb"A+{B}".
 \ttindex{A+\{B\}}
 
 \begin{coq_example*}
-Inductive sumor (A:Set) (B:Prop) : Set := inleft (_:A) | inright (_:B).
+Inductive sumor (A:Set) (B:Prop) : Set :=
+| inleft (_:A)
+| inright (_:B).
 \end{coq_example*}
 
 We may define variants of the axiom of choice, like in Martin-Löf's
@@ -675,7 +678,8 @@ induction principle.
 
 \begin{coq_example*}
 Theorem nat_case :
- forall (n:nat) (P:nat -> Prop), P 0 -> (forall m:nat, P (S m)) -> P n.
+ forall (n:nat) (P:nat -> Prop), 
+ P 0 -> (forall m:nat, P (S m)) -> P n.
 \end{coq_example*}
 \begin{coq_eval}
 Abort All.
diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex
index d5c6dbfdb..5b447f350 100644
--- a/doc/refman/RefMan-ltac.tex
+++ b/doc/refman/RefMan-ltac.tex
@@ -22,7 +22,7 @@ problems.
 \def\letclause{\textrm{\textsl{let\_clause}}}
 \def\matchrule{\textrm{\textsl{match\_rule}}}
 \def\contextrule{\textrm{\textsl{context\_rule}}}
-\def\contexthyps{\textrm{\textsl{context\_hyps}}}
+\def\contexthyp{\textrm{\textsl{context\_hyp}}}
 \def\tacarg{\nterm{tacarg}}
 \def\cpattern{\nterm{cpattern}}
 
@@ -166,11 +166,12 @@ is understood as
 \letclause & ::= & {\ident} \sequence{\name}{} {\tt :=} {\tacexpr}\\
 \\
 \contextrule & ::= &
-  \nelist{\contexthyps}{\tt ,} {\tt |-}{\cpattern} {\tt =>} {\tacexpr}\\
+  \nelist{\contexthyp}{\tt ,} {\tt |-}{\cpattern} {\tt =>} {\tacexpr}\\
 & $|$ & {\tt |-} {\cpattern} {\tt =>} {\tacexpr}\\
 & $|$ & {\tt \_ =>} {\tacexpr}\\
 \\
-\contexthyps & ::= & {\name} {\tt :} {\cpattern}\\
+\contexthyp & ::= & {\name} {\tt :} {\cpattern}\\
+             & $|$ & {\name} {\tt :=} {\cpattern} \zeroone{{\tt :} {\cpattern}}\\
 \\
 \matchrule & ::= &
            {\cpattern} {\tt =>} {\tacexpr}\\
@@ -268,31 +269,53 @@ A sequence is an expression of the following form:
 \begin{quote}
 {\tacexpr}$_1$ {\tt ;} {\tacexpr}$_2$
 \end{quote}
-{\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 every subgoal generated by the application of
-$v_1$. Sequence is left-associative.
+The expressions {\tacexpr}$_1$ and {\tacexpr}$_2$ are evaluated
+to $v_1$ and $v_2$ which have to be tactic values. The tactic $v_1$ is
+then applied and $v_2$ is applied to every subgoal generated by the
+application of $v_1$. Sequence is left-associative.
 
 \subsubsection[General sequence]{General sequence\tacindex{;[\ldots$\mid$\ldots$\mid$\ldots]}}
 %\tacindex{; [ | ]}
 %\index{; [ | ]@{\tt ;[\ldots$\mid$\ldots$\mid$\ldots]}}
 \index{Tacticals!; [ \mid ]@{\tt {\tac$_0$};[{\tac$_1$}$\mid$\ldots$\mid$\tac$_n$]}}
 
-We can generalize the previous sequence operator as
+A general sequence has the following form:
 \begin{quote}
 {\tacexpr}$_0$ {\tt ; [} {\tacexpr}$_1$ {\tt |} $...$ {\tt |}
 {\tacexpr}$_n$ {\tt ]}
 \end{quote}
-{\tacexpr}$_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.
+The expressions {\tacexpr}$_i$ are evaluated to $v_i$, for $i=0,...,n$
+and all have to be tactics. The tactic $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.
 
-\variant If no tactic is given for the $i$-th generated subgoal, it
+\begin{Variants}
+  \item If no tactic is given for the $i$-th generated subgoal, it
 behaves as if the tactic {\tt idtac} were given. For instance, {\tt
 split ; [ | auto ]} is a shortcut for
 {\tt split ; [ idtac | auto ]}.
 
+  \item {\tacexpr}$_0$ {\tt ; [} {\tacexpr}$_1$ {\tt |} $...$ {\tt |}
+    {\tacexpr}$_i$ {\tt |} {\tt ..} {\tt |} {\tacexpr}$_{i+1+j}$ {\tt |}
+    $...$ {\tt |} {\tacexpr}$_n$ {\tt ]}
+
+  In this variant, {\tt idtac} is used for the subgoals numbered from
+  $i+1$ to $i+j$ (assuming $n$ is the number of subgoals).
+
+  Note that {\tt ..} is part of the syntax, while $...$ is the meta-symbol used
+  to describe a list of {\tacexpr} of arbitrary length.
+
+  \item {\tacexpr}$_0$ {\tt ; [} {\tacexpr}$_1$ {\tt |} $...$ {\tt |}
+    {\tacexpr}$_i$ {\tt |} {\tacexpr} {\tt ..} {\tt |}
+    {\tacexpr}$_{i+1+j}$ {\tt |} $...$ {\tt |} {\tacexpr}$_n$ {\tt ]}
+
+  In this variant, {\tacexpr} is used instead of {\tt idtac} for the
+  subgoals numbered from $i+1$ to $i+j$.
+
+\end{Variants}
+
+
 
 \subsubsection[For loop]{For loop\tacindex{do}
 \index{Tacticals!do@{\tt do}}}
@@ -591,7 +614,7 @@ We can make pattern matching on goals using the following expression:
 \end{quote}
 
 If each hypothesis pattern $hyp_{1,i}$, with $i=1,...,m_1$
-is matched (non-linear first order unification) by an hypothesis of
+is matched (non-linear first-order unification) by an hypothesis of
 the goal and if {\cpattern}$_1$ is matched by the conclusion of the
 goal, then {\tacexpr}$_1$ is evaluated to $v_1$ by substituting the
 pattern matching to the metavariables and the real hypothesis names
diff --git a/doc/tutorial/Tutorial.tex b/doc/tutorial/Tutorial.tex
index 8944ec979..219706e35 100755
--- a/doc/tutorial/Tutorial.tex
+++ b/doc/tutorial/Tutorial.tex
@@ -108,6 +108,10 @@ $e:\tau(E)$ for the judgment that $e$ is of type $E$.
 You may request \Coq~ to return to you the type of a valid expression by using
 the command \verb:Check::
 
+\begin{coq_eval}
+Set Printing Width 60.
+\end{coq_eval}
+
 \begin{coq_example}
 Check O.
 \end{coq_example}
@@ -169,9 +173,9 @@ arrow function constructor, in order to get a functional type
 \begin{coq_example}
 Check (nat -> Prop).
 \end{coq_example}
-which may be composed again with \verb:nat: in order to obtain the
+which may be composed one more times with \verb:nat: in order to obtain the
 type \verb:nat->nat->Prop: of binary relations over natural numbers.
-Actually \verb:nat->nat->Prop: is an abbreviation for 
+Actually the type \verb:nat->nat->Prop: is an abbreviation for 
 \verb:nat->(nat->Prop):. 
 
 Functional notions may be composed in the usual way. An expression $f$
@@ -213,7 +217,7 @@ argument \verb:m: of type \verb:nat: in order to build its result as
 \begin{coq_example}
 Definition double (m:nat) := plus m m.
 \end{coq_example}
-This definition introduces the constant \texttt{double} defined as the
+This introduces the constant \texttt{double} defined as the
 expression \texttt{fun m:nat => plus m m}.
 The abstraction introduced by \texttt{fun} is explained as follows. The expression
 \verb+fun x:A => e+ is well formed of type \verb+A->B+ in a context
@@ -445,7 +449,6 @@ conjunctive goal into the two subgoals:
 \begin{coq_example}
 split.
 \end{coq_example}
-
 and the proof is now trivial. Indeed, the whole proof is obtainable as follows:
 \begin{coq_example}
 Restart.
@@ -540,7 +543,7 @@ explanations. The \texttt{fun} prefix, such as \verb+fun H:A\/B =>+,
 corresponds
 to \verb:intro H:, whereas a subterm such as 
 \verb:(or_intror: \verb:B H0):
-corresponds to the sequence \verb:apply or_intror; exact H0:. 
+corresponds to the sequence of tactics \verb:apply or_intror; exact H0:. 
 The generic combinator \verb:or_intror: needs to be instantiated by
 the two properties \verb:B: and \verb:A:. Because \verb:A: can be
 deduced from the type of \verb:H0:, only  \verb:B: is printed.
@@ -559,7 +562,7 @@ Qed.
 
 \subsection{Classical reasoning}
 
-\verb:tauto: always comes back with an answer. Here is an example where it 
+The tactic \verb:tauto: always comes back with an answer. Here is an example where it 
 fails:
 \begin{coq_example}
 Lemma Peirce : ((A -> B) -> A) -> A.
@@ -661,6 +664,9 @@ remove a section, or we may return to the initial state using~:
 \begin{coq_example}
 Reset Initial.
 \end{coq_example}
+\begin{coq_eval}
+Set Printing Width 60.
+\end{coq_eval}
 
 We shall now declare a new \verb:Section:, which will allow us to define
 notions local to a well-delimited scope. We start by assuming a domain of
@@ -705,7 +711,7 @@ predicate as argument:
 Check ex.
 \end{coq_example}
 and the notation \verb+(exists x:D, P x)+ is just concrete syntax for 
-\verb+(ex D (fun x:D => P x))+. 
+the expression \verb+(ex D (fun x:D => P x))+. 
 Existential quantification is handled in \Coq~ in a similar
 fashion to the connectives \verb:/\: and \verb:\/: : it is introduced by
 the proof combinator \verb:ex_intro:, which is invoked by the specific 
@@ -842,7 +848,8 @@ elim (EM (exists x, ~ P x)).
 
 We first look at the first case. Let Tom be the non-drinker:
 \begin{coq_example}
-intro Non_drinker; elim Non_drinker; intros Tom Tom_does_not_drink.
+intro Non_drinker; elim Non_drinker;
+  intros Tom Tom_does_not_drink.
 \end{coq_example}
 
 We conclude in that case by considering Tom, since his drinking leads to
@@ -1026,7 +1033,8 @@ predicates over some universe \verb:U:. For instance:
 Variable U : Type.
 Definition set := U -> Prop.
 Definition element (x:U) (S:set) := S x.
-Definition subset (A B:set) := forall x:U, element x A -> element x B.
+Definition subset (A B:set) := 
+  forall x:U, element x A -> element x B.
 \end{coq_example}
 
 Now, assume that we have loaded a module of general properties about
@@ -1151,7 +1159,7 @@ right; trivial.
 \end{coq_example}
 
 Indeed, the whole proof can be done with the combination of the
-\verb:simple induction: tactic, which combines \verb:intro: and \verb:elim:,
+ \verb:simple: \verb:induction:, which combines \verb:intro: and \verb:elim:,
 with good old \verb:auto::
 \begin{coq_example}
 Restart.
@@ -1197,13 +1205,15 @@ an expression to its {\sl normal form}:
 \begin{coq_example}
 Eval cbv beta in
   ((fun _:nat => nat) O ->
-   (forall y:nat, (fun _:nat => nat) y -> (fun _:nat => nat) (S y)) ->
+   (forall y:nat, 
+      (fun _:nat => nat) y -> (fun _:nat => nat) (S y)) ->
    forall n:nat, (fun _:nat => nat) n).
 \end{coq_example}
 
 Let us now show how to program addition with primitive recursion:
 \begin{coq_example}
-Definition addition (n m:nat) := prim_rec m (fun p rec:nat => S rec) n.
+Definition addition (n m:nat) :=
+    prim_rec m (fun p rec:nat => S rec) n.
 \end{coq_example}
 
 That is, we specify that \verb+(addition n m)+ computes by cases on \verb:n:
@@ -1242,6 +1252,9 @@ Reset bool.
 \begin{coq_eval}
 Reset Initial.
 \end{coq_eval}
+\begin{coq_eval}
+Set Printing Width 60.
+\end{coq_eval}
 
 Let us now show how to do proofs by structural induction. We start with easy
 properties of the \verb:plus: function we just defined. Let us first
@@ -1508,13 +1521,13 @@ development is not type-checked again.
 
 \section{Creating your own modules}
 
-You may create your own modules, by writing \Coq~ commands in a file,
+You may create your own module files, by writing {\Coq} commands in a file,
 say \verb:my_module.v:. Such a module may be simply loaded in the current
 context, with command \verb:Load my_module:. It may also be compiled,
 in ``batch'' mode, using the UNIX command
 \verb:coqc:. Compiling the module \verb:my_module.v: creates a 
 file \verb:my_module.vo:{} that can be reloaded with command
-\verb:Require Import my_module:. 
+\verb:Require: \verb:Import: \verb:my_module:. 
 
 If a required module depends on other modules then the latters are
 automatically required beforehand. However their contents is not
diff --git a/lib/pp_control.ml b/lib/pp_control.ml
index 67ae4a20a..7617d5ca4 100644
--- a/lib/pp_control.ml
+++ b/lib/pp_control.ml
@@ -105,5 +105,7 @@ let set_depth_boxes v =
 
 let get_margin () = Some (Format.pp_get_margin !std_ft ())
 let set_margin v =
-  Format.pp_set_margin !std_ft (match v with None -> default_margin | Some v -> v)
+  let v = match v with None -> default_margin | Some v -> v in
+  Format.pp_set_margin !std_ft v;
+  Format.pp_set_margin !deep_ft v
 
diff --git a/theories/Logic/Hurkens.v b/theories/Logic/Hurkens.v
index 46a574322..71c9af50b 100644
--- a/theories/Logic/Hurkens.v
+++ b/theories/Logic/Hurkens.v
@@ -19,7 +19,7 @@
       and Applications (TLCA'95), 1995.
 
     - [Geuvers] "Inconsistency of Classical Logic in Type Theory", 2001
-      (see www.cs.kun.nl/~herman/note.ps.gz).
+      (see http://www.cs.kun.nl/~herman/note.ps.gz).
 *)
 
 Section Paradox.