From a22efd21eb7e2ddf4e5678631a1ea6ff2824d314 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 30 Jan 2015 14:07:29 +0100
Subject: A few refinements in whodidwhat 8.4.
---
doc/whodidwhat/whodidwhat-8.4update.tex | 19 +++++++++++++------
1 file changed, 13 insertions(+), 6 deletions(-)
(limited to 'doc')
diff --git a/doc/whodidwhat/whodidwhat-8.4update.tex b/doc/whodidwhat/whodidwhat-8.4update.tex
index 696fff4f74..36efd22e96 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 Why 3)
\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
From 9bbf64143da7c29a3b7b1bf84a70f887e1e8aa63 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Tue, 10 Feb 2015 23:04:29 +0100
Subject: Avoid html markup inside tex files and fix url.
---
doc/whodidwhat/whodidwhat-8.4update.tex | 3 ++-
1 file changed, 2 insertions(+), 1 deletion(-)
(limited to 'doc')
diff --git a/doc/whodidwhat/whodidwhat-8.4update.tex b/doc/whodidwhat/whodidwhat-8.4update.tex
index 36efd22e96..bb4c5ce469 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}
@@ -333,7 +334,7 @@
\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 Why 3)
+ from Claude Marché (now integrated to \href{http://why3.lri.fr/}{Why3})
\end{itemize}
For oversights or accidental errors, please report to Hugo~\verb=.=~Herbelin~\verb=@=~inria~\verb=.=~fr
--
cgit v1.2.3