aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--doc/common/macros.tex3
-rw-r--r--doc/refman/RefMan-ext.tex24
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 1d423f8b1..4530c7174 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}