Corrections diverses

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

8 files changed, 19 insertions, 14 deletions

diff --git a/doc/Cases.tex b/doc/Cases.tex
index cb9ff0963b..badc48dce0 100644
--- a/doc/Cases.tex
+++ b/doc/Cases.tex
@@ -377,11 +377,12 @@ been:
 
 \begin{coq_example}
 Reset concat.
-Fixpoint concat [n:nat; l:(listn n)] : (m:nat) (listn m) -> (listn (plus n m)) 
-:= [m:nat][l':(listn m)] 
+Fixpoint concat [n:nat; l:(listn n)]
+     : (m:nat) (listn m) -> (listn (plus n m)) :=
+  [m:nat][l':(listn m)] 
     <[n,_:nat](listn (plus n m))>Cases l l' of 
-                     niln          x => x
-                  | (consn n' a y) x => (consn (plus n' m) a (concat n' y m x))
+          niln          x => x
+       | (consn n' a y) x => (consn (plus n' m) a (concat n' y m x))
                   end.
 \end{coq_example}
 
@@ -551,7 +552,8 @@ Here is a summary of the error messages corresponding to each situation:
 
   \begin{itemize}
   \item {\tt Unable to infer a Cases predicate\\
-Either there is a type incompatiblity or the problem involves dependencies}
+    Either there is a type incompatiblity or the problem involves\\
+    dependencies}
   \end{itemize}
 
   Then the user should provide an elimination predicate.
diff --git a/doc/Correctness.tex b/doc/Correctness.tex
index 6021ec9a76..7c8d97fc52 100644
--- a/doc/Correctness.tex
+++ b/doc/Correctness.tex
@@ -659,7 +659,7 @@ following:
     \texttt{Exchange}).
 
   \item[Sorted]: this  module defines the property  for an array to be
-    sorted, on the whole  array  (\texttt{sorted\_array}) or on a  segment
+    sorted, either on the whole  array  (\texttt{sorted\_array}) or on a  segment
     (\texttt{sub\_sorted\_array}). It  also   provides  a few   lemmas  to
     establish this property.
 \end{description}
diff --git a/doc/RefMan-cic.tex b/doc/RefMan-cic.tex
index 483fedbb87..4fd12e0f2d 100755
--- a/doc/RefMan-cic.tex
+++ b/doc/RefMan-cic.tex
@@ -579,8 +579,8 @@ $\Gamma_C$.
 The occurrences of the variables of $\Gamma_P$ in the contexts
 $\Gamma_I$ and $\Gamma_C$ are bound.
 
-The definition \Ind{\Gamma}{\Gamma_P}{\;\Gamma_I}{\Gamma_C\;} will be
-well-formed exactly when \NInd{\Gamma,\Gamma_P}{\;\Gamma_I}{\Gamma_C\;} is.
+The definition \Ind{\Gamma}{\Gamma_P}{\Gamma_I}{\Gamma_C} will be
+well-formed exactly when \NInd{\Gamma,\Gamma_P}{\Gamma_I}{\Gamma_C} is.
 If $\Gamma_P$ is $[p_1:P_1;\ldots;p_r:P_r]$, an object in 
 \Ind{\Gamma}{\Gamma_P}{\Gamma_I}{\Gamma_C} applied to $q_1,\ldots,q_r$
 will behave as the corresponding object of 
diff --git a/doc/RefMan-ext.tex b/doc/RefMan-ext.tex
index 1085733141..72413f8919 100644
--- a/doc/RefMan-ext.tex
+++ b/doc/RefMan-ext.tex
@@ -722,6 +722,8 @@ Check (p r1 r2).
 \end{coq_example}
 
 \subsubsection{Explicit Applications}
+\comindex{Explicitation of implicit arguments}
+\label{Implicits-explicitation}
 
 The mechanism of synthesis of implicit arguments is not complete, so
 we have sometimes to give explicitly certain implicit arguments of an
diff --git a/doc/RefMan-gal.tex b/doc/RefMan-gal.tex
index 45a055c3bc..9691af050e 100644
--- a/doc/RefMan-gal.tex
+++ b/doc/RefMan-gal.tex
@@ -575,7 +575,7 @@ as a postulate.
 \item {\tt Parameter {\ident} : {\term}.}
   \comindex{Parameter}\\
   Is equivalent to {\tt Axiom {\ident} : {\term}}
-\item {\tt Parameter \nelist{\nelist{\ident}{,} : {\term}}{;} {\tt .}} \\
+\item {\tt Parameter \nelist{\nelistwithoutblank{\ident}{,} : {\term}}{;} {\tt .}} \\
 %        Is equivalent to {\tt Axiom {\lident} : {\term}}  
   Links the {\term}'s to the names comprising the lists \nelist{\nelist{\ident}{,} : {\term}}{;}.
 \end{Variants}
diff --git a/doc/RefMan-pro.tex b/doc/RefMan-pro.tex
index a1c189d914..03f01d8d7d 100755
--- a/doc/RefMan-pro.tex
+++ b/doc/RefMan-pro.tex
@@ -251,7 +251,7 @@ This command displays the current goals.
   Displays the whole list of tactics applied from the beginning
   of the current proof. 
   This tactics script may contain some holes (subgoals not yet proved).
-  They are printed as \verb!<Your Tactic Text here>!.
+  They are printed under the form \verb!<Your Tactic Text here>!.
 
 \item {\tt Show Tree.}\comindex{Show Tree}\\
 This command can be seen as a more structured way of
diff --git a/doc/RefMan-syn.tex b/doc/RefMan-syn.tex
index 11e0b9af7f..790c7c27c3 100755
--- a/doc/RefMan-syn.tex
+++ b/doc/RefMan-syn.tex
@@ -856,7 +856,7 @@ Grammar tactic ne_identarg_list : ast list :=
 Note that the grammar type must be recalled in every extension
 command, or else the system could not discriminate between a single
 AST and an AST list with only one item. If omitted, the default type
-depends on the universe name. The following command fails because {\tt
+depends on the universe name. The following command fails because the non-terminal {\tt
 ne\_identarg\_list} is already defined with type {\tt ast list} but the
 {\tt Grammar} command header assumes its type is {\tt ast}.
 
diff --git a/doc/RefMan-tacex.tex b/doc/RefMan-tacex.tex
index b7f9680b3f..c74206ab6b 100644
--- a/doc/RefMan-tacex.tex
+++ b/doc/RefMan-tacex.tex
@@ -463,7 +463,8 @@ Variable g:nat->nat->nat.
 Axiom g0:(m:nat)(g (0) m)=m.
 Axiom g1:
   (n,m:nat)(gt n (0))->(gt m (100))->(g n m)=(g (pred n) (minus m (10))).
-Axiom g2:(n,m:nat)(gt n (0))->(le m (100))->(g n m)=(g (S n) (plus m (11))).
+Axiom g2:
+  (n,m:nat)(gt n (0))->(le m (100))->(g n m)=(g (S n) (plus m (11))).
 \end{coq_example*}
 
 \begin{coq_example}
@@ -496,7 +497,7 @@ language \texttt{L} of
 'abstract terms' and a type \texttt{A} of 'concrete terms' 
 and a function \texttt{f : L -> A}. If \texttt{L} is a simple
 inductive datatype and \texttt{f} a simple fixpoint, \texttt{Quote f}
-will replace the head of current goal a convertible term with the form 
+will replace the head of current goal by a convertible term of the form 
 \texttt{(f t)}. \texttt{L} must have a constructor of type: \texttt{A
   -> L}. 
 
@@ -642,7 +643,7 @@ Quote interp_f [A B].
 Undo. Quote interp_f [B C iff]. 
 \end{coq_example}
 
-\Warning  This tactic is new and experimental. Since function inversion
+\Warning Since function inversion
 is undecidable in general case, don't expect miracles from it!
 
 % \SeeAlso file \texttt{theories/DEMOS/DemoQuote.v}