Imported Upstream version 8.5~beta2+dfsgupstream/8.5_beta2+dfsg

2 files changed, 21 insertions, 6 deletions

diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template
index 854c786c..024e1341 100644
--- a/doc/stdlib/index-list.html.template
+++ b/doc/stdlib/index-list.html.template
@@ -476,6 +476,13 @@ through the <tt>Require Import</tt> command.</p>
     theories/MSets/MSetPositive.v
     theories/MSets/MSetToFiniteSet.v
     (theories/MSets/MSets.v)
+    theories/MMaps/MMapAVL.v
+    theories/MMaps/MMapFacts.v
+    theories/MMaps/MMapInterface.v
+    theories/MMaps/MMapList.v
+    theories/MMaps/MMapPositive.v
+    theories/MMaps/MMapWeakList.v
+    (theories/MMaps/MMaps.v)
   </dd>
 
   <dt> <b>FSets</b>:
diff --git a/doc/whodidwhat/whodidwhat-8.4update.tex b/doc/whodidwhat/whodidwhat-8.4update.tex
index 696fff4f..bb4c5ce4 100644
--- a/doc/whodidwhat/whodidwhat-8.4update.tex
+++ b/doc/whodidwhat/whodidwhat-8.4update.tex
@@ -3,6 +3,7 @@
 \usepackage{fullpage}
 \usepackage[utf8]{inputenc}
 \usepackage{t1enc}
+\usepackage{hyperref}
 
 \begin{document}
 
@@ -32,7 +33,7 @@
   \end{itemize}
 \item The universe hierarchy
   \begin{itemize}
-  \item Floating universes: Gérard Huet, with contributions from Bruno Barras
+  \item Floating universes: Gérard Huet, with contributions from Bruno Barras and Pierre Letouzey
   \item Algebraic universes: Hugo Herbelin
   \end{itemize}
 \item Mutual inductive types and recursive definitions
@@ -296,10 +297,15 @@
 \section{Maintenance and system engineering}
 
 \begin{itemize}
-\item General bug support: Gérard Huet, Christine Paulin, Chet Murthy,
-  Jean-Christophe Filliâtre, Hugo Herbelin, Bruno Barras, Pierre
-  Letouzey with contributions at some time from Benjamin Werner,
-  Jean-Marc Notin, Pierre Boutillier, ...
+%\item General maintenance in version 8.0: Bruno Barras, Hugo Herbelin
+%\item General maintenance in version 8.1: Bruno Barras, Hugo Herbelin, Jean-Marc Notin
+%\item General maintenance in version 8.2: Hugo Herbelin, Pierre Letouzey, Jean-Marc Notin, 
+%\item General maintenance in version 8.3: Hugo Herbelin, Pierre
+%  Letouzey
+\item General maintenance in version 8.4: Pierre Letouzey, Hugo
+  Herbelin, Pierre Boutillier, Matthieu Sozeau, Stéphane Glondu with
+  contributions from Guillaume Melquiond, Julien Narboux and
+  Pierre-Marie Pédrot
 \item Team coordination: Gérard Huet, Christine Paulin, Hugo Herbelin,
   with various other contributions
 \item Packaging tools: Henri Laulhere, David Delahaye, Julien Narboux,
@@ -327,8 +333,10 @@
 \begin{itemize}
 \item Searching modulo isomorphism: David Delahaye
 \item Explanation of proofs in pseudo-natural language: Yann Coscoy
+\item Dp: Jean-Christophe Filliâtre, Nicolas Ayache with contributions
+  from Claude Marché (now integrated to \href{http://why3.lri.fr/}{Why3})
 \end{itemize}
 
-For probable oversights or accidental errors, please report to Hugo~\verb=.=~Herbelin~\verb=@=~inria~\verb=.=~fr
+For oversights or accidental errors, please report to Hugo~\verb=.=~Herbelin~\verb=@=~inria~\verb=.=~fr
 
 \end{document}