- 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

4 files changed, 54 insertions, 27 deletions

diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex
index 8b404f4efa..501f9b0b17 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 3a4d7f03e6..48c18e265e 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 d158590479..24eb3d1123 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 d5c6dbfdb9..5b447f3500 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