From 0aa2544d04dbd4b6ee665b551ed165e4fb02d2fa Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 15 Jul 2015 10:36:12 +0200 Subject: Imported Upstream version 8.5~beta2+dfsg --- doc/stdlib/index-list.html.template | 7 +++++++ doc/whodidwhat/whodidwhat-8.4update.tex | 20 ++++++++++++++------ 2 files changed, 21 insertions(+), 6 deletions(-) (limited to 'doc') 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 Require Import command.

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)
FSets: 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} -- cgit v1.2.3