Merge PR#422: Supporting all kinds of binders, including 'pat, in syntax of record fields.

2 files changed, 21 insertions, 6 deletions

diff --git a/doc/common/macros.tex b/doc/common/macros.tex
index 5abdecfc1..0a4251a37 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 74d64497a..6dd0ddf81 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}