From 9d27ae09786866b6e3d7b79d1fa7667e5e2aa309 Mon Sep 17 00:00:00 2001
From: Stephane Glondu
Date: Tue, 19 Apr 2011 16:44:20 +0200
Subject: Imported Upstream version 8.3.pl2
---
doc/refman/RefMan-ext.tex | 10 +++++-----
doc/refman/RefMan-oth.tex | 17 ++++++++++++++++-
doc/stdlib/index-list.html.template | 4 ++--
3 files changed, 23 insertions(+), 8 deletions(-)
(limited to 'doc')
diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex
index b8a893d5..c0e578fe 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 $jRequire Import command.
theories/FSets/FMapFullAVL.v
-
+
Reals:
Formalization of real numbers
--
cgit v1.2.3