diff options
| author | herbelin | 2011-04-06 17:00:43 +0000 |
|---|---|---|
| committer | herbelin | 2011-04-06 17:00:43 +0000 |
| commit | b2b2292949b04ec7d114addd487f6e0a94003914 (patch) | |
| tree | ef01c0c08af1c648fecb1ee3618198e16c829c98 | |
| parent | 9600a6960debedbe1bc941aff383fab37a546b94 (diff) | |
Fixing bug #2475 (ability to use binders in the syntax of fields was not in doc)
(backport from 8.3)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13961 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | doc/refman/RefMan-ext.tex | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex index 62875be0d0..98c4b7fae1 100644 --- a/doc/refman/RefMan-ext.tex +++ b/doc/refman/RefMan-ext.tex @@ -24,8 +24,8 @@ construction allows to define ``signatures''. && ~~~~\zeroone{\ident} \verb!{! \zeroone{\nelist{\field}{;}} \verb!}! \verb:.:\\ & & \\ -{\field} & ::= & {\name} : {\type} [ {\tt where} {\it notation} ] \\ - & $|$ & {\name} {\typecstr} := {\term} +{\field} & ::= & {\name} \zeroone{\binders} : {\type} [ {\tt where} {\it notation} ] \\ + & $|$ & {\name} \zeroone{\binders} {\typecstr} := {\term} \end{tabular} \end{centerframe} \caption{Syntax for the definition of {\tt Record}} @@ -37,9 +37,9 @@ construction allows to define ``signatures''. \smallskip {\tt Record} {\ident} {\params} \texttt{:} {\sort} := {\ident$_0$} \verb+{+ - {\ident$_1$} \texttt{:} {\term$_1$}; + {\ident$_1$} \binders$_1$ \texttt{:} {\term$_1$}; \dots - {\ident$_n$} \texttt{:} {\term$_n$} \verb+}+. + {\ident$_n$} \binders$_n$ \texttt{:} {\term$_n$} \verb+}+. \smallskip \noindent the identifier {\ident} is the name of the defined record @@ -47,7 +47,7 @@ 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. If {\sort} is omitted, the default sort is ``{\Type}''. The identifiers {\ident$_1$}, .., -{\ident$_n$} are the names of fields and {\term$_1$}, .., {\term$_n$} +{\ident$_n$} are the names of fields and {\tt forall} \binders$_1${\tt ,} {\term$_1$}, ..., {\tt forall} \binders$_n${\tt ,} {\term$_n$} their respective types. Remark that the type of {\ident$_i$} may depend on the previous {\ident$_j$} (for $j<i$). Thus the order of the fields is important. Finally, {\params} are the parameters of the |