*** empty log message ***

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

4 files changed, 81 insertions, 169 deletions

diff --git a/doc/RefMan-ext.tex b/doc/RefMan-ext.tex
index 7f521f308..a5cc9f7e4 100644
--- a/doc/RefMan-ext.tex
+++ b/doc/RefMan-ext.tex
@@ -17,17 +17,15 @@ construction allows to define ``signatures''.
 \begin{figure}
 \begin{tabular}{|lcl|}
 \hline
-{\sentence} & ::= & {\record}\\
+{\sentence} & ++= & {\record}\\
   & & \\
-{\record} & ::= &  {\tt Record} {\ident} {\binderlet} {\tt :} {\sort}
+{\record} & ::= &  {\tt Record} {\ident} \sequence{\binderlet}{} {\tt :} {\sort}
     \verb.:=. \zeroone{\ident} \verb!{! 
     \zeroone{\nelist{\field}{;}}
     \verb!}! \verb:.:\\
   & & \\
-{\field} & ::= & {\ident} \verb.:. {\type} \\
- & $|$ & {\ident} \verb.:=. {\term} \\
- & $|$ & {\ident} \verb.:. {\type} \verb.:=. {\term} \\
- & $|$ & {\ident} \verb.:=. {\term} \verb.:. {\type} \\
+{\field} & ::= & {\name} \verb.:. {\type} \\
+ & $|$ & {\name} {\typecstr} \verb.:=. {\term} \\
 \hline
 \end{tabular}
 \caption{Syntax for the definition of {\tt Record}}
@@ -37,16 +35,16 @@ construction allows to define ``signatures''.
 \noindent In the expression
 
 \smallskip
-{\tt Record} {\ident} {\tt [} {\params} {\tt ]} \texttt{:} 
+{\tt Record} {\ident} {\params} \texttt{:} 
    {\sort} := {\ident$_0$} \verb+{+
  {\ident$_1$} \texttt{:} {\term$_1$}; 
               \dots
   {\ident$_n$} \texttt{:} {\term$_n$} \verb+}+.
 \smallskip
  
-\noindent the identifier {\ident} is the name of the defined record and {\sort}
-is its type. The identifier {\ident$_0$} is the name of its
-constructor. If {\ident$_0$} is omitted, the default name {\tt
+\noindent the identifier {\ident} is the name of the defined record
+and {\sort} is its type. The identifier {\ident$_0$} is the name of
+its constructor. If {\ident$_0$} is omitted, the default name {\tt
 Build\_{\ident}} is used. The identifiers {\ident$_1$}, ..,
 {\ident$_n$} are the names of fields and {\term$_1$}, .., {\term$_n$}
 their respective types. Remark that the type of {\ident$_i$} may
@@ -57,8 +55,10 @@ record.
 More generally, a record may have explicitly defined (a.k.a.
 manifest) fields. For instance, {\tt Record} {\ident} {\tt [}
 {\params} {\tt ]} \texttt{:} {\sort} := \verb+{+ {\ident$_1$}
-\texttt{:} {\type$_1$} \verb+;+ {\ident$_2$} \texttt{:=} {\term$_2$} \verb+;+
-{\ident$_3$} \texttt{:} {\type$_3$} \verb+}+ in which case the correctness of {\type$_3$} may rely on the instance {\term$_2$}  of  {\ident$_2$} and  {\term$_2$}  in turn may depend on {\ident$_1$}.
+\texttt{:} {\type$_1$} \verb+;+ {\ident$_2$} \texttt{:=} {\term$_2$}
+\verb+;+ {\ident$_3$} \texttt{:} {\type$_3$} \verb+}+ in which case
+the correctness of {\type$_3$} may rely on the instance {\term$_2$} of
+{\ident$_2$} and {\term$_2$} in turn may depend on {\ident$_1$}.
 
 
 \Example
@@ -79,24 +79,16 @@ Record Rat : Set := mkRat
 Remark here that the field
 \verb+Rat_cond+ depends on the field \verb+bottom+. 
 
-Let us now see the work done by the {\tt Record} macro.
-First the macro generates an inductive definition
-with just one constructor:
+Let us now see the work done by the {\tt Record} macro.  First the
+macro generates an inductive definition with just one constructor:
 
 \medskip
 \noindent
-{\tt Inductive {\ident} {\binderlet} : {\sort} := \\
-\mbox{}\hspace{0.4cm} {\ident$_0$} : forall ({\ident$_1$}:{\term$_1$}) .. 
-({\ident$_n$}:{\term$_n$}), {\ident} {\rm\sl params}.}
-\medskip
-
-or, equivalently,
-
-\medskip
-\noindent
-{\tt Inductive {\ident} {\binderlet} : {\sort} := \\
-\mbox{}\hspace{0.4cm} {\ident$_0$} ({\ident$_1$}:{\term$_1$}) .. 
-({\ident$_n$}:{\term$_n$}).}
+\begin{tabular}{l}
+{\tt Inductive {\ident} {\params} :{\sort} :=} \\
+~~~~{\tt
+  {\ident$_0$} ({\ident$_1$}:{\term$_1$}) .. ({\ident$_n$}:{\term$_n$}).}
+\end{tabular}
 \medskip
 
 
diff --git a/doc/RefMan-gal.tex b/doc/RefMan-gal.tex
index 7700bbfe6..264987c50 100644
--- a/doc/RefMan-gal.tex
+++ b/doc/RefMan-gal.tex
@@ -96,45 +96,6 @@ sequence of any characters different from \verb!"! or the sequence
 \verb!""! to denote the double quote character. In grammars, the
 entry for quoted strings is {\qstring}.
 
-
-%% \begin{center}
-%% \begin{tabular}{|l|l|}
-%% \hline
-%% Sequence        & Character denoted \\
-%% \hline
-%% \verb"\\"       & backslash (\verb"\") \\
-%% \verb'\"'       & double quote (\verb'"') \\
-%% \verb"\n"       & newline (LF) \\
-%% \verb"\r"       & return (CR) \\
-%% \verb"\t"       & horizontal tabulation (TAB) \\
-%% \verb"\b"       & backspace (BS) \\
-%% \verb"\"$ddd$  & the character with ASCII code $ddd$ in decimal \\
-%% \hline
-%% \end{tabular}
-%% \end{center}
-
-%% Strings can be split on several lines using a backslash (\verb!\!)  at
-%% the end of each line, just before the newline. For instance,
-
-%% \begin{flushleft}
-%% \begin{small}
-%% \begin{verbatim}
-%% Add LoadPath "/usr/local/coq/\
-%% contrib/Rocq/LAMBDA".
-%% \end{verbatim}
-%% \end{small}
-%% \end{flushleft}
-      
-%% is correctly parsed, and equivalent to
-
-%% \begin{flushleft}
-%% \begin{small}
-%% \begin{verbatim}
-%% Add LoadPath "/usr/local/coq/contrib/Rocq/LAMBDA".
-%% \end{verbatim}
-%% \end{small}
-%% \end{flushleft}
-
 \paragraph{Keywords}
 The following identifiers are reserved keywords, and cannot be
 employed otherwise:
@@ -173,83 +134,6 @@ employed otherwise:
 \end{tabular}
 \end{center}
 
-%% Hard to maintain...
-
-%% Although they are not considered as keywords, it is not advised to use
-%% words of the following list as identifiers:
-%% \begin{center}
-%% \begin{tabular}{lllll}
-%% \verb!Add!        &
-%% \verb!AddPath!    &
-%% \verb!Abort!      &
-%% \verb!Abstraction!&
-%% \verb!All!        \\
-%% \verb!Begin!      &
-%% \verb!Cd!         &
-%% \verb!Chapter!    &
-%% \verb!Check!      &
-%% \verb!Compute!    \\
-%% % \verb!Conjectures! \\ que dans Show Conjectures sans conflit avec ident
-%% \verb!Defined!    &
-%% \verb!DelPath!    &
-%% \verb!Drop!       &
-%% \verb!End!        &
-%% \verb!Eval!       \\
-%% % \verb!Explain!  n'est pas documente 
-%% \verb!Extraction! &
-%% \verb!Fact!       &
-%% \verb!Focus!      &
-%% % \verb!for! n'intervient que pour Scheme ... Induction ... sans conflit
-%% % \verb!Go! n'est pas documente et semble peu robuste aux erreurs
-%% \verb!Goal!       &
-%% \verb!Guarded!    \\
-%% \verb!Hint!       &
-%% \verb!Immediate!  &
-%% \verb!Induction!  &
-%% \verb!Infix!      &
-%% \verb!Inspect!    \\
-%% \verb!Lemma!      &
-%% \verb!Let!        &
-%% \verb!LoadPath!   &
-%% \verb!Local!      &
-%% \verb!Minimality! \\
-%% \verb!ML!         &
-%% \verb!Module!     &
-%% \verb!Modules!    &
-%% \verb!Mutual!     &
-%% % \verb!Node!   que dans Show Node sans conflit avec ident
-%% \verb!Opaque!     \\
-%% \verb!Parameters! &
-%% \verb!Print!      &
-%% \verb!Pwd!        &
-%% \verb!Remark!     &
-%% \verb!Remove!     \\
-%% \verb!Require!    &
-%% \verb!Reset!      &
-%% \verb!Restart!    &
-%% \verb!Restore!    &
-%% \verb!Resume!     \\
-%% \verb!Save!       &
-%% \verb!Scheme!     &
-%% % \verb!Script!  que dans Show Script sans conflit avec ident
-%% \verb!Search!     &
-%% \verb!Section!    &
-%% \verb!Show!       \\
-%% \verb!Silent!     &
-%% \verb!State!      &
-%% \verb!States!     &
-%% \verb!Suspend!    &
-%% \verb!Syntactic!  \\
-%% \verb!Test!       &
-%% \verb!Transparent!&
-%% % \verb!Tree! que dans Show Tree et Explain Proof Tree sans conflit avec id
-%% \verb!Undo!       &
-%% \verb!Unset!      &
-%% \verb!Unfocus!    \\
-%% \verb!Variables!  &
-%% \verb!Write!      & & &
-%% \end{tabular}
-%% \end{center}
 
 \paragraph{Special tokens}
 The following sequences of characters are special tokens:
@@ -309,7 +193,8 @@ The following sequences of characters are special tokens:
 \verb!|-!  &
 \verb!||!  &
 \verb!}!   &
-\verb!~!   \\\end{tabular}
+\verb!~!   \\
+\end{tabular}
 \end{center}
 
 Lexical ambiguities are resolved according to the ``longest match''
@@ -341,7 +226,8 @@ chapter \ref{Addoc-syntax}.
  & $|$ & {\tt let fix} {\fixpointbody} {\tt in} {\term} &(\ref{fixpoints})\\
  & $|$ & {\tt let cofix} {\cofixpointbody}
          {\tt in} {\term} &(\ref{fixpoints})\\
- & $|$ & {\tt let} {\tt (} \sequence{\name}{,} {\tt) :=} {\term}
+ & $|$ & {\tt let} {\tt (} \sequence{\name}{,} {\tt )} {\returntype}
+         {\tt :=} {\term}
          {\tt in} {\term}  &(\ref{caseanalysis}, \ref{Mult-match})\\
  & $|$ & {\tt if} {\ifitem} {\tt then} {\term}
          {\tt else} {\term} &(\ref{caseanalysis}, \ref{Mult-match})\\
@@ -689,14 +575,14 @@ and ends with a dot.
             & $|$ & {\statement} \zeroone{\proof} \\
 &&\\
 %% Declarations
-{\declaration} & ::= & {\declarationkeyword} {\params} {\tt .} \\
+{\declaration} & ::= & {\declarationkeyword} {\assums} {\tt .} \\
 &&\\
 {\declarationkeyword} & ::= & {\tt Axiom} $|$ {\tt Conjecture} \\
   & $|$  & {\tt Parameter} $|$  {\tt Parameters} \\
   & $|$  & {\tt Variable}  $|$ {\tt Variables}  \\
   & $|$  & {\tt Hypothesis}  $|$ {\tt Hypotheses}\\
 &&\\
-{\params} & ::= & \nelist{\ident}{} {\tt :} {\term} \\
+{\assums} & ::= & \nelist{\ident}{} {\tt :} {\term} \\
           & $|$ & \nelist{\binder}{} \\
 &&\\
 %% Definitions
diff --git a/doc/RefMan-lib.tex b/doc/RefMan-lib.tex
index c9173870d..13f9bd64f 100755
--- a/doc/RefMan-lib.tex
+++ b/doc/RefMan-lib.tex
@@ -847,45 +847,77 @@ module {\tt ZArith} and opening scope {\tt Z\_scope}.
 \ttindex{?=}
 \ttindex{mod}
 
-Figure~\ref{zarith-syntax} shows the notations provided by {\tt
-Z\_scope}. It specifies how notations are interpreted and, when not
-already reserved, the precedence and associativity.
-
 \begin{figure}
 \begin{center}
 \begin{tabular}{l|l|l|l}
 Notation & Interpretation & Precedence & Associativity\\
 \hline
-\verb!_ < _! & {\tt Zlt} \\
-\verb!x <= y! & {\tt Zle} \\
-\verb!_ > _! & {\tt Zgt} \\
-\verb!x >= y! & {\tt Zge} \\
-\verb!x < y < z! & {\tt x < y \verb!/\! y < z} \\
-\verb!x < y <= z! & {\tt x < y \verb!/\! y <= z} \\
-\verb!x <= y < z! & {\tt x <= y \verb!/\! y < z} \\
-\verb!x <= y <= z! & {\tt x <= y \verb!/\! y <= z} \\
+\verb!_ < _! & {\tt Zlt} &&\\
+\verb!x <= y! & {\tt Zle} &&\\
+\verb!_ > _! & {\tt Zgt} &&\\
+\verb!x >= y! & {\tt Zge} &&\\
+\verb!x < y < z! & {\tt x < y \verb!/\! y < z} &&\\
+\verb!x < y <= z! & {\tt x < y \verb!/\! y <= z} &&\\
+\verb!x <= y < z! & {\tt x <= y \verb!/\! y < z} &&\\
+\verb!x <= y <= z! & {\tt x <= y \verb!/\! y <= z} &&\\
 \verb!_ ?= _! & {\tt Zcompare} & 70 & no\\
-\verb!_ + _! & {\tt Zplus} \\
-\verb!_ - _! & {\tt Zminus} \\
-\verb!_ * _! & {\tt Zmult} \\
-\verb!_ / _! & {\tt Zdix} \\
+\verb!_ + _! & {\tt Zplus} &&\\
+\verb!_ - _! & {\tt Zminus} &&\\
+\verb!_ * _! & {\tt Zmult} &&\\
+\verb!_ / _! & {\tt Zdiv} &&\\
 \verb!_ mod _! & {\tt Zmod} & 40 & no \\
-\verb!- _!  & {\tt Zopp} \\
-\verb!_ ^ _! & {\tt Zpower} \\
+\verb!- _!  & {\tt Zopp} &&\\
+\verb!_ ^ _! & {\tt Zpower} &&\\
 \end{tabular}
 \end{center}
 \label{zarith-syntax}
 \caption{Definition of the scope for integer arithmetics ({\tt Z\_scope})}
 \end{figure}
 
+Figure~\ref{zarith-syntax} shows the notations provided by {\tt
+Z\_scope}. It specifies how notations are interpreted and, when not
+already reserved, the precedence and associativity.
+
+\begin{coq_example}
+Require Import ZArith.
+Check  (2 + 3)%Z.
+Open Scope Z_scope.
+Check 2 + 3.
+\end{coq_example}
+
 \subsection{Peano's arithmetic (\texttt{nat})}
 \index{Peano's arithmetic}
+\ttindex{nat\_scope}
 
 While in the initial state, many operations and predicates of Peano's
 arithmetic are defined, further operations and results belong to other
 modules. For instance, the decidability of the basic predicates are
 defined here. This is provided by requiring the module {\tt Arith}.
 
+Figure~\ref{nat-syntax} describes notation available in scope {\tt
+nat\_scope}.
+
+\begin{figure}
+\begin{center}
+\begin{tabular}{l|l}
+Notation & Interpretation \\
+\hline
+\verb!_ < _! & {\tt lt} \\
+\verb!x <= y! & {\tt le} \\
+\verb!_ > _! & {\tt gt} \\
+\verb!x >= y! & {\tt ge} \\
+\verb!x < y < z! & {\tt x < y \verb!/\! y < z} \\
+\verb!x < y <= z! & {\tt x < y \verb!/\! y <= z} \\
+\verb!x <= y < z! & {\tt x <= y \verb!/\! y < z} \\
+\verb!x <= y <= z! & {\tt x <= y \verb!/\! y <= z} \\
+\verb!_ + _! & {\tt plus} \\
+\verb!_ - _! & {\tt minus} \\
+\verb!_ * _! & {\tt mult} \\
+\end{tabular}
+\end{center}
+\label{nat-syntax}
+\caption{Definition of the scope for natural numbers ({\tt nat\_scope})}
+\end{figure}
 
 \subsection{Real numbers library}
 
@@ -897,8 +929,8 @@ opening scope {\tt R\_scope}. This set of notations is very similar to
 the notation for integer arithmetics. The inverse function was added.
 \begin{figure}
 \begin{center}
-\begin{tabular}{l|l|l|l}
-Notation & Interpretation & Precedence & Associativity\\
+\begin{tabular}{l|l}
+Notation & Interpretation \\
 \hline
 \verb!_ < _! & {\tt Rlt} \\
 \verb!x <= y! & {\tt Rle} \\
@@ -911,7 +943,7 @@ Notation & Interpretation & Precedence & Associativity\\
 \verb!_ + _! & {\tt Rplus} \\
 \verb!_ - _! & {\tt Rminus} \\
 \verb!_ * _! & {\tt Rmult} \\
-\verb!_ / _! & {\tt Rdix} \\
+\verb!_ / _! & {\tt Rdiv} \\
 \verb!- _!  & {\tt Ropp} \\
 \verb!/ _!  & {\tt Rinv} \\
 \verb!_ ^ _! & {\tt pow} \\
@@ -1011,6 +1043,7 @@ can be accessed by requiring module {\tt List}.
 It defines the following notions:
 \begin{center}
 \begin{tabular}{l|l}
+\hline
 {\tt length} & length \\
 {\tt head} & first element (with default) \\
 {\tt tail} & all but first element \\
@@ -1021,6 +1054,7 @@ It defines the following notions:
 {\tt flat\_map} & applying a function returning lists \\
 {\tt fold\_left} & iterator (from head to tail) \\
 {\tt fold\_right} & iterator (from tail to head) \\
+\hline
 \end{tabular}
 \end{center}
 
diff --git a/doc/macros.tex b/doc/macros.tex
index e2b4c20ff..5dc7f4947 100755
--- a/doc/macros.tex
+++ b/doc/macros.tex
@@ -93,6 +93,7 @@
 
 %% New syntax specific entries
 \newcommand{\annotation}{\nterm{annotation}}
+\newcommand{\assums}{\nterm{assums}} % vernac
 \newcommand{\binder}{\nterm{binder}}
 \newcommand{\binderlet}{\nterm{binderlet}}
 \newcommand{\binderlist}{\nterm{binderlist}}
@@ -136,7 +137,6 @@
 \newcommand{\form}{\textrm{\textsl{form}}}
 \newcommand{\entry}{\textrm{\textsl{entry}}} 
 \newcommand{\symbolentry}{\textrm{\textsl{symbol}}}
-\newcommand{\localassums}{\textrm{\textsl{local\_assums}}}
 \newcommand{\localdef}{\textrm{\textsl{local\_def}}}
 \newcommand{\localdecls}{\textrm{\textsl{local\_decls}}}
 \newcommand{\ident}{\textrm{\textsl{ident}}}