Typos/coq-tex/divers

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

2 files changed, 58 insertions, 23 deletions

diff --git a/doc/RefMan-gal.tex b/doc/RefMan-gal.tex
index 5a4983151..8be425c13 100644
--- a/doc/RefMan-gal.tex
+++ b/doc/RefMan-gal.tex
@@ -381,7 +381,8 @@ subclass of the syntactic class {\term}.
 \index{specif@{\specif}}
 \item {\Type} is the type of {\Set} and {\Prop}
 \end{itemize}
-More on sorts can be found in section \ref{Sorts}.
+More on sorts can be found in section~\ref{Sorts}.
+\noindent More on sorts can be found in section \ref{Sorts}.
 
 \subsection{Binders
 \label{Binders}
@@ -737,7 +738,6 @@ environment}\index{Environment}.
 A formal presentation of constants and environments is given in
 Section~\ref{Typed-terms}.
 
-
 \subsubsection{\tt Definition {\ident} := {\term}.
 \comindex{Definition}}
 
@@ -770,22 +770,22 @@ environment, provided that {\term} is well-typed.
 
 \SeeAlso Sections \ref{Opaque}, \ref{Transparent}, \ref{unfold}
 
-\subsubsection{\tt Local {\ident} := {\term}.
-\comindex{Local}}
+\subsubsection{\tt Let {\ident} := {\term}.
+\comindex{Let}}
 
 This command binds the value {\term} to the name {\ident} in the
-environment of the current section. The name {\ident} will be unknown
-when the current section will be closed and all occurrences of
-{\ident} in persistent objects (such as theorems) defined within the
-section will be replaced by \term.  One can say that the {\tt Local}
-definition is a kind of {\em macro}.
+environment of the current section. The name {\ident} disappears
+when the current section is eventually closed, and, all
+persistent objects (such as theorems) defined within the
+section and depending on {\ident} are prefixed by the local definition
+{\tt let {\ident} := {\term} in}.
 
 \begin{ErrMsgs}
 \item \errindex{Clash with previous constant {\ident}}
 \end{ErrMsgs}
 
 \begin{Variants}
-\item {\tt Local {\ident} : {\term$_1$} := {\term$_2$}.}
+\item {\tt Let {\ident} : {\term$_1$} := {\term$_2$}.}
 \end{Variants}
 
 \SeeAlso Sections \ref{Section} (section mechanism), \ref{Opaque},
@@ -831,7 +831,7 @@ for {\ident}.  This condition ensures the soundness of the inductive
 definition.  If this is the case, the constants {\ident},
 {\ident$_1$}, {\ldots}, {\ident$_n$} are added to the environment with
 their respective types.  Accordingly to the universe where
-the inductive type lives({\it e.g.} its type {\sort}), {\Coq} provides a
+the inductive type lives ({\it e.g.} its type {\sort}), {\Coq} provides a
 number of destructors for {\ident}.  Destructors are named
 {\ident}{\tt\_ind}, {\ident}{\tt \_rec} or {\ident}{\tt \_rect} which
 respectively correspond to elimination principles on {\tt Prop}, {\tt
@@ -919,10 +919,10 @@ induction principle we got for {\tt nat}.
 
 \begin{ErrMsgs}
 \item \errindex{Non strictly positive occurrence of {\ident} in {\type}}
-\item \errindex{Type of Constructor not well-formed}
+\item \errindex{The conclusion of {\type} is not valid; it must be
+built from {\ident}}
 \end{ErrMsgs}
 
-
 \subsubsection{Parameterized inductive types}
 
 Inductive types may be parameterized. Parameters differ from inductive
@@ -939,21 +939,21 @@ The general scheme is:
 
 A typical example is the definition of polymorphic lists:
 \begin{coq_example*}
-Inductive list (X:Set) : Set :=
-  | Nil : list X
-  | Cons : X -> list X -> list X.
+Inductive list (A:Set) : Set :=
+  | nil : list A
+  | cons : A -> list A -> list A.
 \end{coq_example*}
 
-Note that in the type of {\tt Nil} and {\tt Cons}, we write {\tt
-  (list X)} and not just {\tt list}.\\ The constants {\tt Nil} and
-{\tt Cons} will have respectively types:
+Note that in the type of {\tt nil} and {\tt cons}, we write {\tt
+  (list A)} and not just {\tt list}.\\ The constants {\tt nil} and
+{\tt cons} will have respectively types:
 
 \begin{coq_example}
-Check Nil.
-Check Cons.
+Check nil.
+Check cons.
 \end{coq_example}
 
-Types of destructors will be also quantified with {\tt (X:Set)}.
+Types of destructors are also quantified with {\tt (A:Set)}.
 
 \begin{coq_eval}
 Reset Initial.
@@ -961,12 +961,16 @@ Reset Initial.
 \begin{Variants}
 \item
 \begin{coq_example*}
-Inductive list (X:Set) : Set := Nil | Cons (_:X) (_:list X).
+Inductive list (A:Set) : Set := nil | cons (_:X) (_:list X).
 \end{coq_example*}
 This is an alternative definition of lists where we specify the
 arguments of the constructors rather than their full type.
 \end{Variants}
 
+\begin{ErrMsgs}
+\item \errindex{The {\num}th argument of {\ident} must be {\ident'} in {\type}}
+\end{ErrMsgs}
+
 \SeeAlso Sections~\ref{Cic-inductive-definitions} and~\ref{elim}.
 
 
diff --git a/doc/RefMan-syn.tex b/doc/RefMan-syn.tex
index 12ca5fc10..c948f25f8 100755
--- a/doc/RefMan-syn.tex
+++ b/doc/RefMan-syn.tex
@@ -135,16 +135,46 @@ Notation "x = y" := (@eq ? x y) (at level 70, no associativity).
 One can define {\em closed} notations whose both sides are symbols. In
 this case, the default precedence level for inner subexpression is 200.
 
+\begin{coq_eval}
+Set Printing Depth 50.
+(********** The following is correct but produces **********)
+(**** an incompatibility with the reserved notation ********)
+\end{coq_eval}
 \begin{coq_example*}
 Notation "{ A } + { B }" := (sumbool A B) (at level 0).
 \end{coq_example*}
 
 One can also define notations for binders.
 
+\begin{coq_eval}
+Set Printing Depth 50.
+(********** The following is correct but produces **********)
+(**** an incompatibility with the reserved notation ********)
+\end{coq_eval}
 \begin{coq_example*}
 Notation "{ x : A  |  P }" := (sig A (fun x => P)) (at level 0).
 \end{coq_example*}
 
+In the last case though, there is a conflict with the notation for
+type casts. This notation, as shown by the command {\tt Print Grammar
+constr} is at level 100. To avoid $x:A$ being parsed at a type cast,
+it is necessary to put {\tt x} at a level below 100, typically 99. Hence, a
+correct definition is 
+
+\begin{coq_example*}
+Notation "{ x : A  |  P }" := (sig A (fun x => P)) (at level 0, x at level 99).
+\end{coq_example*}
+
+This change has retrospectively an effect on the notation for notation
+{\tt "{ A } + { B }"}. For the sake of factorisation, {\tt A} must be
+put at level 99 too, which gives
+
+\begin{coq_example*}
+Notation "{ A } + { B }" := (sumbool A B) (at level 0, A at level 99).
+\end{coq_example*}
+
+See the next section for more about factorisation.
+
 \subsection{Simple factorisation rules}
 
 {\Coq} extensible parsing is performed by Camlp4 which is essentially a
@@ -527,6 +557,7 @@ interpreted in the scope stack extended with the scope bound to
 {\nterm{key}}.
 
 To bind a delimiting key to a scope, use the command
+
 \begin{quote}
 \texttt{Delimit Scope} {\scope} \texttt{with} {\ident} 
 \end{quote}