Imported Upstream version 8.3.pl2upstream/8.3.pl2

3 files changed, 23 insertions, 8 deletions

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 $j<i$). Thus the order of the
 fields is important. Finally, {\params} are the parameters of the
diff --git a/doc/refman/RefMan-oth.tex b/doc/refman/RefMan-oth.tex
index 920e86de..025788f5 100644
--- a/doc/refman/RefMan-oth.tex
+++ b/doc/refman/RefMan-oth.tex
@@ -929,6 +929,21 @@ the command has not terminated after the time specified by the integer
 (time expressed in seconds), then it is interrupted and an error message
 is displayed.
 
+\subsection[\tt Set Default Timeout \textrm{\textsl{int}}.]{\tt Set
+  Default Timeout \textrm{\textsl{int}}.\comindex{Set Default Timeout}}
+
+After using this command, all subsequent commands behave as if they
+were passed to a {\tt Timeout} command. Commands already starting by
+a {\tt Timeout} are unaffected.
+
+\subsection[\tt Unset Default Timeout.]{\tt Unset Default Timeout.\comindex{Unset Default Timeout}}
+
+This command turns off the use of a defaut timeout.
+
+\subsection[\tt Test Default Timeout.]{\tt Test Default Timeout.\comindex{Test Default Timeout}}
+
+This command displays whether some default timeout has be set or not.
+
 \section{Controlling display}
 
 \subsection[\tt Set Silent.]{\tt Set Silent.\comindex{Set Silent}
@@ -1173,7 +1188,7 @@ control the scope of their effect. There are four kinds of commands:
 \end{itemize}
 
 
-% $Id: RefMan-oth.tex 13454 2010-09-23 17:00:29Z aspiwack $ 
+% $Id: RefMan-oth.tex 13923 2011-03-21 16:25:20Z letouzey $ 
 
 %%% Local Variables: 
 %%% mode: latex
diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template
index 7ee85fe8..541fa1b9 100644
--- a/doc/stdlib/index-list.html.template
+++ b/doc/stdlib/index-list.html.template
@@ -452,13 +452,13 @@ through the <tt>Require Import</tt> command.</p>
     theories/FSets/FMapFullAVL.v
   </dd>
 
-<!--  <dt> <b>Strings</b>
+  <dt> <b>Strings</b>
     Implementation of string as list of ascii characters
   </dt>
   <dd>
     theories/Strings/Ascii.v
     theories/Strings/String.v
-  </dd> -->
+  </dd>
     
   <dt> <b>Reals</b>:
     Formalization of real numbers