Documenting the grammar {| ... |} syntax for building records.

And an extra minor changes (use of zeroone when relevant, use of type
rather than term).

2 files changed, 21 insertions, 6 deletions

diff --git a/doc/common/macros.tex b/doc/common/macros.tex
index 5abdecfc18..0a4251a373 100644
--- a/doc/common/macros.tex
+++ b/doc/common/macros.tex
@@ -145,7 +145,7 @@
 
 \newcommand{\typecstr}{\zeroone{{\tt :}~{\term}}}
 \newcommand{\typecstrwithoutblank}{\zeroone{{\tt :}{\term}}}
-
+\newcommand{\typecstrtype}{\zeroone{{\tt :}~{\type}}}
 
 \newcommand{\Fwterm}{\nterm{Fwterm}}
 \newcommand{\Index}{\nterm{index}}
@@ -164,6 +164,7 @@
 \newcommand{\digit}{\nterm{digit}}
 \newcommand{\exteqn}{\nterm{ext\_eqn}}
 \newcommand{\field}{\nterm{field}}
+\newcommand{\fielddef}{\nterm{field\_def}}
 \newcommand{\firstletter}{\nterm{first\_letter}}
 \newcommand{\fixpg}{\nterm{fix\_pgm}}
 \newcommand{\fixpointbodies}{\nterm{fix\_bodies}}
diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex
index 1d423f8b16..4530c71742 100644
--- a/doc/refman/RefMan-ext.tex
+++ b/doc/refman/RefMan-ext.tex
@@ -29,8 +29,8 @@ construction allows defining ``signatures''.
 {\recordkw} & ::= &
    {\tt Record} $|$ {\tt Inductive} $|$ {\tt CoInductive}\\
   & & \\
-{\field} & ::= & {\name} \zeroone{\binders} : {\type} [ {\tt where} {\it notation} ] \\
- & $|$ & {\name} \zeroone{\binders} {\typecstr} := {\term}
+{\field} & ::= & {\name} \zeroone{\binders} : {\type} \zeroone{{\tt where} {\it notation}} \\
+ & $|$ & {\name} \zeroone{\binders} {\typecstrtype} := {\term}\\
 \end{tabular}
 \end{centerframe}
 \caption{Syntax for the definition of {\tt Record}}
@@ -213,7 +213,21 @@ Record point := { x : nat; y : nat }.
 Definition a := Build_point 5 3.
 \end{coq_example}
 
-The following syntax allows creating objects by using named fields. The
+\begin{figure}[t]
+\begin{centerframe}
+\begin{tabular}{lcl}
+{\term} & ++= &
+         \verb!{|! \zeroone{\nelist{\fielddef}{;}} \verb!|}! \\
+  & & \\
+{\fielddef} & ::= & {\name} \zeroone{\binders} := {\term} \\
+\end{tabular}
+\end{centerframe}
+\caption{Syntax for constructing elements of a \texttt{Record} using named fields}
+\label{fig:fieldsyntax}
+\end{figure}
+
+A syntax is available for creating objects by using named fields, as
+shown on Figure~\ref{fig:fieldsyntax}. The
 fields do not have to be in any particular order, nor do they have to be all
 present if the missing ones can be inferred or prompted for (see
 Section~\ref{Program}).
@@ -252,7 +266,7 @@ Eval compute in (
 Reset Initial.
 \end{coq_eval}
 
-\Rem An experimental syntax for projections based on a dot notation is
+\Rem A syntax for projections based on a dot notation is
 available. The command to activate it is
 \optindex{Printing Projections}
 \begin{quote}
@@ -267,7 +281,7 @@ available. The command to activate it is
  & $|$ & {\term} {\tt .(} {@}{\qualid} \nelist{\term}{} {\tt )}
 \end{tabular}
 \end{centerframe}
-\caption{Syntax of \texttt{Record} projections}
+\caption{Syntax for \texttt{Record} projections}
 \label{fig:projsyntax}
 \end{figure}