diff options
author | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-01-30 14:07:29 +0100 |
---|---|---|
committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-02-10 19:09:09 +0100 |
commit | a22efd21eb7e2ddf4e5678631a1ea6ff2824d314 (patch) | |
tree | db8c10456d2a5e91b01ddde5980f908844146cb4 /doc/whodidwhat | |
parent | c3d6651262a3ef8651de0c738e88b0f8ed34fdc2 (diff) |
A few refinements in whodidwhat 8.4.
Diffstat (limited to 'doc/whodidwhat')
-rw-r--r-- | doc/whodidwhat/whodidwhat-8.4update.tex | 19 |
1 files changed, 13 insertions, 6 deletions
diff --git a/doc/whodidwhat/whodidwhat-8.4update.tex b/doc/whodidwhat/whodidwhat-8.4update.tex index 696fff4f7..36efd22e9 100644 --- a/doc/whodidwhat/whodidwhat-8.4update.tex +++ b/doc/whodidwhat/whodidwhat-8.4update.tex @@ -32,7 +32,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 +296,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 +332,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 <a href="why.lri.fr">Why 3</a>) \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} |