From 7cfc4e5146be5666419451bdd516f1f3f264d24a Mon Sep 17 00:00:00 2001
From: Enrico Tassi <gareuselesinge@debian.org>
Date: Sun, 25 Jan 2015 14:42:51 +0100
Subject: Imported Upstream version 8.5~beta1+dfsg

---
 doc/LICENSE                                  |   6 +-
 doc/common/styles/html/coqremote/footer.html |   6 +-
 doc/common/styles/html/coqremote/header.html |  34 ++-
 doc/common/styles/html/simple/header.html    |   6 +-
 doc/stdlib/Library.tex                       |   2 +
 doc/stdlib/hidden-files                      |   1 +
 doc/stdlib/index-list.html.template          |  95 ++++----
 doc/stdlib/make-library-files                |  36 ---
 doc/stdlib/make-library-index                |   8 +-
 doc/whodidwhat/whodidwhat-8.2update.tex      | 303 +++++++++++++++++++++++
 doc/whodidwhat/whodidwhat-8.3update.tex      | 312 ++++++++++++++++++++++++
 doc/whodidwhat/whodidwhat-8.4update.tex      | 334 ++++++++++++++++++++++++++
 doc/whodidwhat/whodidwhat-8.5update.tex      | 346 +++++++++++++++++++++++++++
 13 files changed, 1379 insertions(+), 110 deletions(-)
 delete mode 100755 doc/stdlib/make-library-files
 create mode 100644 doc/whodidwhat/whodidwhat-8.2update.tex
 create mode 100644 doc/whodidwhat/whodidwhat-8.3update.tex
 create mode 100644 doc/whodidwhat/whodidwhat-8.4update.tex
 create mode 100644 doc/whodidwhat/whodidwhat-8.5update.tex

(limited to 'doc')

diff --git a/doc/LICENSE b/doc/LICENSE
index 99087480..ada22e66 100644
--- a/doc/LICENSE
+++ b/doc/LICENSE
@@ -8,7 +8,7 @@ forth in the Open Publication License, v1.0 or later (the latest
 version is presently available at http://www.opencontent.org/openpub/).
 Options A and B are *not* elected.
 
-The Coq Tutorial is a work by Gérard Huet, Gilles Kahn and Christine
+The Coq Tutorial is a work by Gérard Huet, Gilles Kahn and Christine
 Paulin-Mohring. All documents (the LaTeX source and the PostScript,
 PDF and html outputs) are copyright (c) INRIA 1999-2006. The material
 connected to the Coq Tutorial may be distributed only subject to the
@@ -25,7 +25,7 @@ the PostScript, PDF and html outputs) are copyright (c) INRIA
 distributed under the terms of the Lesser General Public License
 version 2.1 or later. 
 
-The FAQ (Coq for the Clueless) is a work by Pierre Castéran, Hugo
+The FAQ (Coq for the Clueless) is a work by Pierre Castéran, Hugo
 Herbelin, Florent Kirchner, Benjamin Monate, and Julien Narboux. All
 documents (the LaTeX source and the PostScript, PDF and html outputs)
 are copyright (c) INRIA 2004-2006. The material connected to the FAQ
@@ -36,7 +36,7 @@ http://www.opencontent.org/openpub/). Options A and B are *not*
 elected.
 
 The Tutorial on [Co-]Inductive Types in Coq is a work by Pierre
-Castéran and Eduardo Gimenez. All related documents (the LaTeX and
+Castéran and Eduardo Gimenez. All related documents (the LaTeX and
 BibTeX sources and the PostScript, PDF and html outputs) are copyright
 (c) INRIA 1997-2006. The material connected to the Tutorial on
 [Co-]Inductive Types in Coq may be distributed only subject to the
diff --git a/doc/common/styles/html/coqremote/footer.html b/doc/common/styles/html/coqremote/footer.html
index ff38ba8a..23dfccb6 100644
--- a/doc/common/styles/html/coqremote/footer.html
+++ b/doc/common/styles/html/coqremote/footer.html
@@ -21,9 +21,9 @@
   <div id="footer">
     <div id="nav-footer">
       <ul class="links-menu-footer">
-        <li><a href="mailto:www-coq_@_lix.polytechnique.fr">webmaster</a></li>
-        <li><a href="http://validator.w3.org/check?uri=referer">xhtml valid</a></li>
-        <li><a href="http://jigsaw.w3.org/css-validator/check/referer">CSS valid</a></li>
+        <li><a href="mailto:coq-www_@_inria.fr">webmaster</a></li>
+        <li><a href="http://validator.w3.org/">xhtml valid</a></li>
+        <li><a href="http://jigsaw.w3.org/css-validator/">CSS valid</a></li>
       </ul>
     </div>
   </div>
diff --git a/doc/common/styles/html/coqremote/header.html b/doc/common/styles/html/coqremote/header.html
index 891fb328..c6c45091 100644
--- a/doc/common/styles/html/coqremote/header.html
+++ b/doc/common/styles/html/coqremote/header.html
@@ -2,18 +2,16 @@
 <html xmlns="http://www.w3.org/1999/xhtml" lang="en" xml:lang="en">
 
 <head>
-<meta http-equiv="Content-Type" content="text/html; charset=ISO-8859-1">
-<title>Standard Library | The Coq Proof Assistant</title>
-
-<link rel="shortcut icon" href="favicon.ico" type="image/x-icon" />
-<style type="text/css" media="all">@import "http://coq.inria.fr/modules/node/node.css";</style>
+<meta http-equiv="Content-Type" content="text/html; charset=utf-8" />
+<link rel="shortcut icon" href="/favicon.ico" type="image/x-icon" />
+<link type="text/css" rel="stylesheet" media="all" href="/modules/node/node.css" />
+<link type="text/css" rel="stylesheet" media="all" href="/modules/system/defaults.css" />
+<link type="text/css" rel="stylesheet" media="all" href="/modules/system/system.css" />
+<link type="text/css" rel="stylesheet" media="all" href="/modules/user/user.css" />
+<link type="text/css" rel="stylesheet" media="all" href="/sites/all/themes/coq/style.css" />
+<link type="text/css" rel="stylesheet" media="all" href="/sites/all/themes/coq/coqdoc.css" />
 
-<style type="text/css" media="all">@import "http://coq.inria.fr/modules/system/defaults.css";</style>
-<style type="text/css" media="all">@import "http://coq.inria.fr/modules/system/system.css";</style>
-<style type="text/css" media="all">@import "http://coq.inria.fr/modules/user/user.css";</style>
-
-<style type="text/css" media="all">@import "http://coq.inria.fr/sites/all/themes/coq/style.css";</style>
-<style type="text/css" media="all">@import "http://coq.inria.fr/sites/all/themes/coq/coqdoc.css";</style>
+<title>Standard Library | The Coq Proof Assistant</title>
 
 </head>
 
@@ -23,20 +21,20 @@
   <div id="headertop">
     <div id="nav">
       <ul class="links-menu">
-        <li><a href="http://coq.inria.fr/" class="active">Home</a></li>
-        <li><a href="http://coq.inria.fr/about-coq" title="More about coq">About Coq</a></li>    
-        <li><a href="http://coq.inria.fr/download">Get Coq</a></li>
-        <li><a href="http://coq.inria.fr/documentation">Documentation</a></li>
-        <li><a href="http://coq.inria.fr/community">Community</a></li>
+        <li><a href="/" class="active">Home</a></li>
+        <li><a href="/about-coq" title="More about coq">About Coq</a></li>
+        <li><a href="/download">Get Coq</a></li>
+        <li><a href="/documentation">Documentation</a></li>
+        <li><a href="/community">Community</a></li>
       </ul>
     </div>
   </div>
 
   <div id="header">
     <div id="logoWrapper">
-      <div id="logo"><a href="http://coq.inria.fr/" title="Home"><img src="http://coq.inria.fr/files/barron_logo.png" alt="Home" /></a>
+      <div id="logo"><a href="/" title="Home"><img src="/files/barron_logo.png" alt="Home" /></a>
       </div>
-      <div id="siteName"><a href="http://coq.inria.fr/" title="Home">The Coq Proof Assistant</a>
+      <div id="siteName"><a href="/" title="Home">The Coq Proof Assistant</a>
       </div>
     </div>
   </div>
diff --git a/doc/common/styles/html/simple/header.html b/doc/common/styles/html/simple/header.html
index 14d2f988..c350a8b9 100644
--- a/doc/common/styles/html/simple/header.html
+++ b/doc/common/styles/html/simple/header.html
@@ -1,11 +1,11 @@
-<!DOCTYPE html 
+<!DOCTYPE html
      PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN"
     "http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd">
 
 <html xmlns="http://www.w3.org/1999/xhtml" xml:lang="en" lang="en">
 <head>
-<meta http-equiv="Content-Type" content="text/html; charset=iso-8859-15"/>
-<link rel="stylesheet" href="coqdoc.css" type="text/css"/>
+<meta http-equiv="Content-Type" content="text/html; charset=utf-8" />
+<link rel="stylesheet" href="coqdoc.css" type="text/css" />
 <title>The Coq Standard Library</title>
 </head>
 
diff --git a/doc/stdlib/Library.tex b/doc/stdlib/Library.tex
index cb32adfc..44a0b1d3 100755
--- a/doc/stdlib/Library.tex
+++ b/doc/stdlib/Library.tex
@@ -1,9 +1,11 @@
 \documentclass[11pt]{report}
 
+\usepackage[mathletters]{ucs}
 \usepackage[utf8x]{inputenc}
 \usepackage[T1]{fontenc}
 \usepackage{fullpage}
 \usepackage{amsfonts}
+\usepackage{url}
 \usepackage[color]{../../coqdoc}
 
 \input{../common/version}
diff --git a/doc/stdlib/hidden-files b/doc/stdlib/hidden-files
index e69de29b..8b137891 100644
--- a/doc/stdlib/hidden-files
+++ b/doc/stdlib/hidden-files
@@ -0,0 +1 @@
+
diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template
index 833b5c4c..854c786c 100644
--- a/doc/stdlib/index-list.html.template
+++ b/doc/stdlib/index-list.html.template
@@ -3,7 +3,7 @@
 
 <p>Here is a short description of the Coq standard library, which is
 distributed with the system.
-It provides a set of modules directly available 
+It provides a set of modules directly available
 through the <tt>Require Import</tt> command.</p>
 
 <p>The standard library is composed of the following subdirectories:</p>
@@ -12,27 +12,26 @@ through the <tt>Require Import</tt> command.</p>
   <dt> <b>Init</b>:
     The core library (automatically loaded when starting Coq)
   </dt>
-  <dd> 
+  <dd>
     theories/Init/Notations.v
     theories/Init/Datatypes.v
     theories/Init/Logic.v
     theories/Init/Logic_Type.v
+    theories/Init/Nat.v
     theories/Init/Peano.v
     theories/Init/Specif.v
     theories/Init/Tactics.v
     theories/Init/Wf.v
     (theories/Init/Prelude.v)
   </dd>
-  
+
   <dt> <b>Logic</b>:
-      Classical logic and dependent equality
+      Classical logic, dependent equality, extensionality, choice axioms
   </dt>
   <dd>
     theories/Logic/SetIsType.v
-    theories/Logic/Classical_Pred_Set.v
     theories/Logic/Classical_Pred_Type.v
     theories/Logic/Classical_Prop.v
-    theories/Logic/Classical_Type.v
     (theories/Logic/Classical.v)
     theories/Logic/ClassicalFacts.v
     theories/Logic/Decidable.v
@@ -57,8 +56,11 @@ through the <tt>Require Import</tt> command.</p>
     theories/Logic/IndefiniteDescription.v
     theories/Logic/FunctionalExtensionality.v
     theories/Logic/ExtensionalityFacts.v
+    theories/Logic/WeakFan.v
+    theories/Logic/WKL.v
+    theories/Logic/FinFun.v
   </dd>
-    
+
   <dt> <b>Structures</b>:
        Algebraic structures (types with equality, with order, ...).
        DecidableType* and OrderedType* are there only for compatibility.
@@ -83,7 +85,7 @@ through the <tt>Require Import</tt> command.</p>
   <dt> <b>Bool</b>:
        Booleans (basic functions and results)
   </dt>
-  <dd> 
+  <dd>
     theories/Bool/Bool.v
     theories/Bool/BoolEq.v
     theories/Bool/DecBool.v
@@ -92,12 +94,12 @@ through the <tt>Require Import</tt> command.</p>
     theories/Bool/Zerob.v
     theories/Bool/Bvector.v
   </dd>
-    
+
   <dt> <b>Arith</b>:
     Basic Peano arithmetic
   </dt>
-  <dd> 
-    theories/Arith/Arith_base.v
+  <dd>
+    theories/Arith/PeanoNat.v
     theories/Arith/Le.v
     theories/Arith/Lt.v
     theories/Arith/Plus.v
@@ -107,6 +109,7 @@ through the <tt>Require Import</tt> command.</p>
     theories/Arith/Between.v
     theories/Arith/Peano_dec.v
     theories/Arith/Compare_dec.v
+    (theories/Arith/Arith_base.v)
     (theories/Arith/Arith.v)
     theories/Arith/Min.v
     theories/Arith/Max.v
@@ -173,8 +176,6 @@ through the <tt>Require Import</tt> command.</p>
     theories/ZArith/Zpow_def.v
     theories/ZArith/Zpow_alt.v
     theories/ZArith/Zpower.v
-    theories/ZArith/ZOdiv_def.v
-    theories/ZArith/ZOdiv.v
     theories/ZArith/Zdiv.v
     theories/ZArith/Zquot.v
     theories/ZArith/Zeuclid.v
@@ -206,10 +207,13 @@ through the <tt>Require Import</tt> command.</p>
     theories/QArith/Qminmax.v
   </dd>
 
-  <dt> <b>Numbers</b>: 
+  <dt> <b>Numbers</b>:
     An experimental modular architecture for arithmetic
   </dt>
-    <dt> <b>&nbsp;&nbsp;Prelude</b>: 
+  <dd>
+    <dl>
+    <dt> <b>&nbsp;&nbsp;Prelude</b>:
+    </dt>
     <dd>
     theories/Numbers/BinNums.v
     theories/Numbers/NumPrelude.v
@@ -219,6 +223,7 @@ through the <tt>Require Import</tt> command.</p>
 
     <dt> <b>&nbsp;&nbsp;NatInt</b>:
        Abstract mixed natural/integer/cyclic arithmetic
+    </dt>
     <dd>
     theories/Numbers/NatInt/NZAdd.v
     theories/Numbers/NatInt/NZAddOrder.v
@@ -237,10 +242,10 @@ through the <tt>Require Import</tt> command.</p>
     theories/Numbers/NatInt/NZGcd.v
     theories/Numbers/NatInt/NZBits.v
     </dd>
-    </dt>
 
-    <dt> <b>&nbsp;&nbsp;Cyclic</b>: 
+    <dt> <b>&nbsp;&nbsp;Cyclic</b>:
        Abstract and 31-bits-based cyclic arithmetic
+    </dt>
     <dd>
     theories/Numbers/Cyclic/Abstract/CyclicAxioms.v
     theories/Numbers/Cyclic/Abstract/NZCyclic.v
@@ -259,10 +264,10 @@ through the <tt>Require Import</tt> command.</p>
     theories/Numbers/Cyclic/Int31/Int31.v
     theories/Numbers/Cyclic/ZModulo/ZModulo.v
     </dd>
-    </dt>
 
-    <dt> <b>&nbsp;&nbsp;Natural</b>: 
+    <dt> <b>&nbsp;&nbsp;Natural</b>:
        Abstract and 31-bits-words-based natural arithmetic
+    </dt>
     <dd>
     theories/Numbers/Natural/Abstract/NAdd.v
     theories/Numbers/Natural/Abstract/NAddOrder.v
@@ -293,10 +298,11 @@ through the <tt>Require Import</tt> command.</p>
     theories/Numbers/Natural/BigN/NMake.v
     theories/Numbers/Natural/BigN/NMake_gen.v
     </dd>
-    </dt>
 
-    <dt> <b>&nbsp;&nbsp;Integer</b>: 
-       Abstract and concrete (especially 31-bits-words-based) integer arithmetic
+    <dt> <b>&nbsp;&nbsp;Integer</b>:
+       Abstract and concrete (especially 31-bits-words-based) integer
+       arithmetic
+    </dt>
     <dd>
     theories/Numbers/Integer/Abstract/ZAdd.v
     theories/Numbers/Integer/Abstract/ZAddOrder.v
@@ -323,32 +329,32 @@ through the <tt>Require Import</tt> command.</p>
     theories/Numbers/Integer/BigZ/BigZ.v
     theories/Numbers/Integer/BigZ/ZMake.v
     </dd>
-    </dt>
 
     <dt><b>&nbsp;&nbsp;Rational</b>:
        Abstract and 31-bits-words-based rational arithmetic
+    </dt>
     <dd>
     theories/Numbers/Rational/SpecViaQ/QSig.v
     theories/Numbers/Rational/BigQ/BigQ.v
     theories/Numbers/Rational/BigQ/QMake.v
     </dd>
-    </dt>
-  </dt>
-  
+    </dl>
+  </dd>
+
   <dt> <b>Relations</b>:
        Relations (definitions and basic results)
   </dt>
-  <dd> 
+  <dd>
     theories/Relations/Relation_Definitions.v
     theories/Relations/Relation_Operators.v
     theories/Relations/Relations.v
     theories/Relations/Operators_Properties.v
   </dd>
-    
+
   <dt> <b>Sets</b>:
        Sets (classical, constructive, finite, infinite, powerset, etc.)
   </dt>
-  <dd> 
+  <dd>
     theories/Sets/Classical_sets.v
     theories/Sets/Constructive_sets.v
     theories/Sets/Cpo.v
@@ -372,32 +378,39 @@ through the <tt>Require Import</tt> command.</p>
     theories/Sets/Relations_3.v
     theories/Sets/Uniset.v
   </dd>
-    
+
   <dt> <b>Classes</b>:
-  <dd> 
+  </dt>
+  <dd>
     theories/Classes/Init.v
     theories/Classes/RelationClasses.v
     theories/Classes/Morphisms.v
     theories/Classes/Morphisms_Prop.v
     theories/Classes/Morphisms_Relations.v
     theories/Classes/Equivalence.v
+    theories/Classes/CRelationClasses.v
+    theories/Classes/CMorphisms.v
+    theories/Classes/CEquivalence.v
     theories/Classes/EquivDec.v
     theories/Classes/SetoidTactics.v
     theories/Classes/SetoidClass.v
     theories/Classes/SetoidDec.v
     theories/Classes/RelationPairs.v
+    theories/Classes/DecidableClass.v
   </dd>
 
   <dt> <b>Setoids</b>:
-  <dd> 
+  </dt>
+  <dd>
     theories/Setoids/Setoid.v
   </dd>
-    
+
   <dt> <b>Lists</b>:
     Polymorphic lists, Streams (infinite sequences)
   </dt>
-  <dd> 
+  <dd>
     theories/Lists/List.v
+    theories/Lists/ListDec.v
     theories/Lists/ListSet.v
     theories/Lists/SetoidList.v
     theories/Lists/SetoidPermutation.v
@@ -413,13 +426,14 @@ through the <tt>Require Import</tt> command.</p>
     theories/Vectors/Fin.v
     theories/Vectors/VectorDef.v
     theories/Vectors/VectorSpec.v
+    theories/Vectors/VectorEq.v
     (theories/Vectors/Vector.v)
   </dd>
 
   <dt> <b>Sorting</b>:
     Axiomatizations of sorts
   </dt>
-  <dd> 
+  <dd>
     theories/Sorting/Heap.v
     theories/Sorting/Permutation.v
     theories/Sorting/Sorting.v
@@ -432,7 +446,7 @@ through the <tt>Require Import</tt> command.</p>
   <dt> <b>Wellfounded</b>:
        Well-founded Relations
   </dt>
-  <dd> 
+  <dd>
     theories/Wellfounded/Disjoint_Union.v
     theories/Wellfounded/Inclusion.v
     theories/Wellfounded/Inverse_Image.v
@@ -500,11 +514,11 @@ through the <tt>Require Import</tt> command.</p>
     theories/Strings/Ascii.v
     theories/Strings/String.v
   </dd>
-    
+
   <dt> <b>Reals</b>:
     Formalization of real numbers
   </dt>
-  <dd> 
+  <dd>
     theories/Reals/Rdefinitions.v
     theories/Reals/Raxioms.v
     theories/Reals/RIneq.v
@@ -566,14 +580,13 @@ through the <tt>Require Import</tt> command.</p>
     theories/Reals/SeqSeries.v
     theories/Reals/Sqrt_reg.v
     theories/Reals/Rlogic.v
-    theories/Reals/LegacyRfield.v
     (theories/Reals/Reals.v)
   </dd>
-    
+
   <dt> <b>Program</b>:
     Support for dependently-typed programming.
   </dt>
-  <dd> 
+  <dd>
     theories/Program/Basics.v
     theories/Program/Wf.v
     theories/Program/Subset.v
diff --git a/doc/stdlib/make-library-files b/doc/stdlib/make-library-files
deleted file mode 100755
index c071c4a2..00000000
--- a/doc/stdlib/make-library-files
+++ /dev/null
@@ -1,36 +0,0 @@
-#!/bin/sh
-
-# Needs COQSRC and GALLINA set
-
-# On garde la liste de tous les *.v avec dates dans library.files.ls
-# Si elle a change depuis la derniere fois ou library.files n'existe pas
-# on fabrique des .g (si besoin) et la liste library.files dans 
-# l'ordre de ls -tr des *.vo
-# Ce dernier trie les fichiers dans l'ordre inverse de leur date de création
-# En supposant que make fait son boulot, ca fait un tri topologique du
-# graphe des dépendances
-
-LIBDIRS="Arith PArith NArith ZArith Reals Logic Bool Lists Relations Sets Sorting Wellfounded Setoids Program Classes Numbers"
-
-rm -f library.files.ls.tmp
-(cd $COQSRC/theories; find $LIBDIR -name "*.v" -ls) > library.files.ls.tmp
-if ! test -e library.files || ! cmp library.files.ls library.files.ls.tmp; then
-  mv -f library.files.ls.tmp library.files.ls
-  rm -f library.files; touch library.files
-  ABSOLUTE=`pwd`/library.files
-  cd $COQSRC/theories
-  echo $LIBDIRS
-  for rep in $LIBDIRS ; do
-    (cd $rep
-     echo $rep/intro.tex >> $ABSOLUTE
-     VOFILES=`ls -tr *.vo`
-     for file in $VOFILES ; do
-       VF=`basename $file \.vo`
-       if [ \( ! -e $VF.g \) -o \( $VF.v -nt $VF.g \) ] ; then
-          $GALLINA $VF.v
-       fi
-       echo $rep/$VF.g >> $ABSOLUTE
-     done
-    )
-  done
-fi
diff --git a/doc/stdlib/make-library-index b/doc/stdlib/make-library-index
index 1a70567f..43802efa 100755
--- a/doc/stdlib/make-library-index
+++ b/doc/stdlib/make-library-index
@@ -6,17 +6,14 @@ FILE=$1
 HIDDEN=$2
 
 cp -f $FILE.template tmp
-echo -n Building file index-list.prehtml ...
+echo -n "Building file index-list.prehtml... "
 
 #LIBDIRS="Init Logic Structures Bool Arith PArith NArith ZArith QArith Relations Sets Classes Setoids Lists Vectors Sorting Wellfounded MSets FSets Reals Program Numbers Numbers/Natural/Abstract Numbers/Natural/Peano Numbers/Natural/Binary Numbers/Natural/BigN Numbers/Natural/SpecViaZ Numbers/Integer/Abstract Numbers/Integer/NatPairs Numbers/Integer/Binary Numbers/Integer/SpecViaZ Numbers/Integer/BigZ Numbers/NatInt Numbers/Cyclic/Abstract Numbers/Cyclic/Int31 Numbers/Cyclic/ZModulo Numbers/Cyclic/DoubleCyclic Numbers/Rational/BigQ Numbers/Rational/SpecViaQ Strings"
-LIBDIRS=`find theories/* -type d | sed -e "s:^theories/::"`
+LIBDIRS=`find theories/* -type d ! -name .coq-native | sed -e "s:^theories/::"`
 
 for k in $LIBDIRS; do
     i=theories/$k
-    echo $i
-    
     d=`basename $i`
-    if [ "$d" != "CVS" ]; then
       ls $i | grep -q \.v'$'
       if [ $? = 0 ]; then
 	for j in $i/*.v; do
@@ -46,7 +43,6 @@ for k in $LIBDIRS; do
             fi
 	done
       fi
-    fi
     rm -f tmp2
     sed -e "s/#$d#//" tmp > tmp2
     mv -f tmp2 tmp
diff --git a/doc/whodidwhat/whodidwhat-8.2update.tex b/doc/whodidwhat/whodidwhat-8.2update.tex
new file mode 100644
index 00000000..4f4f0e95
--- /dev/null
+++ b/doc/whodidwhat/whodidwhat-8.2update.tex
@@ -0,0 +1,303 @@
+\documentclass{article}
+
+\usepackage{fullpage}
+\usepackage[utf8]{inputenc}
+\usepackage{t1enc}
+
+\begin{document}
+
+\title{Who did what in the Coq archive?}
+
+\author{The Coq development team}
+
+\maketitle
+
+\centerline{(updated for Coq 8.2)}
+
+\section{The Calculus of Inductive Constructions}
+
+\begin{itemize}
+\item The Calculus of Constructions
+  \begin{itemize}
+  \item Core type-checker: Gérard Huet and Thierry Coquand with
+    optimizations by Chet Murthy, Bruno Barras
+  \item Head reduction functions: Gérard Huet, Christine Paulin, Bruno Barras
+  \end{itemize}
+\item Conversion and reduction
+  \begin{itemize}
+  \item Lazy conversion machine: Bruno Barras
+  \item Transparency/opacity: Bruno Barras
+  \item Bytecode-based conversion: Benjamin Grégoire
+  \item Binary-words retroknowledge: Arnaud Spiwack 
+  \end{itemize}
+\item The universe hierarchy
+  \begin{itemize}
+  \item Floating universes: Gérard Huet, with contributions from Bruno Barras
+  \item Algebraic universes: Hugo Herbelin
+  \end{itemize}
+\item Mutual inductive types and recursive definitions
+  \begin{itemize}
+  \item Type-checking: Christine Paulin
+  \item Positivity condition: Christine Paulin
+  \item Guardness condition for fixpoints: Christine Paulin;
+    extensions by Eduardo Gimenez and Bruno Barras
+  \item Recursively non-uniform parameters: Christine Paulin
+  \item Sort-polymorphism of inductive types: Hugo Herbelin
+  \end{itemize}
+\item Local definitions: Hugo Herbelin
+\item Mutual coinductive types and corecursive definitions: Eduardo Gimenez
+\item Module system
+  \begin{itemize}
+  \item Core system: Jacek Chrz\k{a}szcz
+  \item Inlining: Claudio Sacerdoti Coen and Élie Soubiran
+  \item Module inclusion: Élie Soubiran
+  \item Functorial signature application: Élie Soubiran
+  \item Transparent name space: Élie Soubiran
+  \item Resolution of qualified names: Hugo Herbelin
+  \end{itemize}
+\item Minimalist stand-alone type-checker (\texttt{coqchk}): Bruno Barras
+\end{itemize}
+
+\section{Specification language}
+
+\begin{itemize}
+\item Sections: Gilles Dowek with extra contributions by Gérard
+  Huet, Chet Murthy, Hugo Herbelin
+\item The \texttt{Russell} specifications language, proof obligations (\texttt{Program}): Matthieu Sozeau
+\item Type inference: Chet Murthy, with extra contributions by Bruno
+  Barras, Hugo Herbelin and Matthieu Sozeau
+\item Pattern-matching: Hugo Herbelin on top of a first version by
+  Cristina Cornes
+\item Implicit arguments: Amokrane Saïbi, with extensions by Hugo
+  Herbelin and Matthieu Sozeau
+\item Coercions: Amokrane Saïbi
+\item Records: Amokrane Saïbi with extensions by Arnaud Spiwack and
+  Matthieu Sozeau
+\item Canonical structures: Amokrane Saïbi
+\item Type classes: Matthieu Sozeau
+\item Functional schemes (\texttt{Function}, \texttt{Functional Scheme}, ...): Julien Forest and Pierre Courtieu (preliminary version by Yves Bertot)
+\item Generation of induction schemes: Christine Paulin, Vincent
+  Siles, Matthieu Sozeau
+ \end{itemize}
+
+\section{Tactics}
+
+\subsection{General tactic support}
+
+\begin{itemize}
+\item Proof engine: Chet Murthy (first version by Thierry Coquand)
+\item Ltac: David Delahaye, with extensions by Hugo Herbelin, Bruno Barras, ...
+\item Tactic notations: Hugo Herbelin (first version by Chet Murthy)
+\item Main tactic unification procedure: Chet Murthy with
+  contributions from Hugo Herbelin and Matthieu Sozeau
+\item Mathematical-style language (C-Zar): Pierre Corbineau
+\item Communication with external tools (\texttt{external}): Hugo Herbelin
+
+\end{itemize}
+
+\subsection{Predefined tactics}
+
+\begin{itemize}
+\item Basic tactics (\texttt{intro}, \texttt{apply},
+  \texttt{assumption}, \texttt{exact}): Thierry Coquand, with further
+  collective extensions
+\item Reduction tactics: Christine Paulin (\texttt{simpl}), Bruno
+  Barras (\texttt{cbv}, \texttt{lazy}), ...
+\item Tacticals: Thierry Coquand, Chet Murthy, Eduardo Gimenez, ...
+\item Induction: Christine Paulin (\texttt{elim}, \texttt{case}), Hugo Herbelin (\texttt{induction}, \texttt{destruct}
+\item Refinement (\texttt{refine}): Jean-Christophe Filliâtre
+\item Introduction patterns: Eduardo Gimenez with collective extensions
+\item Forward reasoning: Hugo Herbelin (\texttt{assert}, \texttt{apply in}), Pierre Letouzey (\texttt{specialize}, initial version by Amy Felty)
+\item Rewriting tactics (\texttt{rewrite}): basic version by Christine Paulin,
+  extensions by Jean-Christophe Filliâtre and Pierre Letouzey
+\item Tactics about equivalence properties (\texttt{reflexivity},
+  \texttt{symmetry}, \texttt{transitivity}): Christine Paulin (?),
+\item Equality tactics (\texttt{injection}/\texttt{discriminate}):
+  Cristina Cornes
+\item Inversion tactics (\texttt{inversion}): Cristina Cornes, Chet Murthy
+\item Setoid rewriting: Matthieu Sozeau (first version by Clément
+  Renard, second version by Claudio Sacerdoti Coen), contributions
+  from Nicolas Tabareau
+\item Decision of equality: Eduardo Gimenez
+\item Basic Ltac-level tactics: Pierre Letouzey, Matthieu Sozeau,
+  Evgeny Makarov
+\end{itemize}
+
+\subsection{General automation tactics}
+
+\begin{itemize}
+\item Resolution (\texttt{auto}, \texttt{trivial}): Christine Paulin
+  with extensions from Chet Murthy, Eduardo Gimenez, Patrick
+  Loiseleur (hint bases), Matthieu Sozeau
+\item Resolution with existential variables (\texttt{eauto}): Chet Murthy, Jean-Christophe Filliâtre, with extensions from Matthieu Sozeau
+\item Automatic rewriting (\texttt{autorewrite}): David Delahaye
+\end{itemize}
+
+\subsection{Domain-specific decision tactics}
+
+\begin{itemize}
+\item Congruence closure (\texttt{cc}): Pierre Corbineau
+\item Decision of first-order logic (\texttt{firstorder}): Pierre Corbineau
+\item Simplification of polynomial fractions (\texttt{field}): Laurent
+  Théry and Benjamin Grégoire (first version by David Delahaye and
+  Micaela Mayero)
+\item Simplification of polynomial expressions (\texttt{ring}): Assia
+  Mahboubi, Bruno Barras and Benjamin Grégoire (first version by
+  Samuel Boutin, second version by Patrick Loiseleur)
+\item Decision of systems of linear inequations: Frédéric Besson
+  (\texttt{psatzl}); Loïc Pottier (\texttt{fourier})
+\item Decision of systems of linear inequations over integers:
+  Frédéric Besson (\texttt{lia}); Pierre Crégut (\texttt{omega} and
+  \texttt{romega})
+\item (Partial) decision of systems of polynomical inequations
+  (\texttt{sos}, \texttt{psatz}): Frédéric Besson, with generalization
+  over arbitrary rings by Evgeny Makarov; uses HOL-Light interface to
+  \texttt{csdp} by John Harrisson
+\item Decision/simplification of intuitionistic propositional logic:
+  David Delahaye (\texttt{tauto}, \texttt{intuition}, first version by
+  Cesar Mu\~noz, second version by Chet Murthy), with contributions
+  from Judicaël Courant; Pierre Corbineau (\texttt{rtauto})
+\item Decision/simplification of intuition first-order logic: Pierre
+  Corbineau (\texttt{firstorder})
+\end{itemize}
+
+\section{Extra tools}
+
+\begin{itemize}
+\item Program extraction: Pierre Letouzey (first implementation by
+  Benjamin Werner, second by Jean-Christophe Filliâtre)
+\item Export of context to external communication tools (\texttt{dp}):
+  Nicolas Ayache and Jean-Christophe Filliâtre, with contributions by
+  Claude Marché
+\item Export of terms and environments to XML format: Claudio
+  Sacerdoti Coen, with extensions from Cezary Kaliszyk
+\end{itemize}
+
+\section{Environment management}
+
+\begin{itemize}
+\item Separate compilation: initiated by Chet Murthy
+\item Import/Export: initiated by Chet Murthy
+\item Options management: Hugo Herbelin with contributions by Arnaud Spiwack
+\item Resetting and backtracking: Chet Murthy with contributions from Pierre Courtieu
+\item Searching: Hugo Herbelin, Yves Bertot
+\item Whelp suppport: Hugo Herbelin
+\end{itemize}
+
+\section{Parsing and printing}
+
+\begin{itemize}
+\item General parsing support: Chet Murthy, Bruno Barras, Daniel de Rauglaudre
+\item General printing support: Chet Murthy, Jean-Christophe Filliâtre
+\item Lexing: Daniel de Rauglaudre
+\item Support for UTF-8: Hugo Herbelin, with contributions from Alexandre Miquel
+\item Numerical notations: Hugo Herbelin, Patrick Loiseleur, Micaela Mayero
+\item String notations: Hugo Herbelin
+\item New ``V8'' syntax: Bruno Barras, Hugo Herbelin with contributions by Olivier Desmettre
+\item Abbreviations: Chet Murthy
+\item Notations: Chet Murthy, Hugo Herbelin
+\end{itemize}
+
+\section{Libraries}
+
+\begin{itemize}
+\item Init: collective (initiated by Christine Paulin and Gérard Huet)
+\item Arith: collective (initiated by Christine Paulin)
+\item ZArith: collective (initiated by Pierre Crégut)
+\item Bool: collective (initiated by Christine Paulin)
+\item NArith: Hugo Herbelin, Pierre Letouzey, Evgeny Makarov (out of
+  initial contibution by Pierre Crégut)
+\item Lists: Pierre Letouzey, Jean-Marc Notin (initiated by Christine Paulin)
+\item Reals: Micaela Mayero (axiomatization and main properties), Olivier Desmettre (convergence, derivability, integrals, trigonometric functions), contributions from Russell O'Connor and Cezary Kaliszyk
+\item Relations: Bruno Barras, Cristina Cornes with contributions from
+  Pierre Castéran
+\item Wellfounded: Bruno Barras, Cristina Cornes
+\item FSets: Pierre Letouzey, from initial work with Jean-Christophe Filliâtre, decision tactic for FSets by Aaron Bohannon
+\item Logic: Christine Paulin, Hugo Herbelin, Bruno Barras
+\item Numbers: Evgeny Makarov (abstractions), Laurent Théry and Benjamin Grégoire (big numbers), Arnaud Spiwack and Pierre Letouzey (word-based arithmetic)
+\item Classes: Matthieu Sozeau
+\item QArith: Pierre Letouzey, with contributions from Russell O'Connor
+\item Setoid: Matthieu Sozeau (first version by Clément Renard, second version by Claudio Sacerdoti Coen)
+\item Sets: Gilles Kahn and Gérard Huet
+\item Sorting: Gérard Huet
+\item Strings: Laurent Théry
+\item Program: Matthieu Sozeau
+\item Unicode: Claude Marché
+\end{itemize}
+
+\section{Commands}
+
+\begin{itemize}
+\item Batch compiler (\texttt{coqc}):  Chet Murthy (?)
+\item Compilation dependency calculator (\texttt{coqdep}):
+  Jean-Christophe Filliâtre
+\item Statistic tool (\texttt{coqwc}): Jean-Christophe Filliâtre
+\item Simple html presentation tool (\texttt{gallina}) (deprecated): Jean-Christophe Filliâtre
+\item Auto-maker (\texttt{coq\_makefile}): Jean-Christophe Filliâtre,
+  with contributions from Judicaël Courant
+\item LaTeX presentation tool (\texttt{coq-tex}): Jean-Christophe Filliâtre
+\item Multi-purpose presentation tool (\texttt{coqdoc}): Jean-Christophe Filliâtre with extensions from
+  Matthieu Sozeau, Jean-Marc Notin, Hugo Herbelin
+\item Interactive toplevel (\texttt{coqtop}): Jean-Christophe Filliâtre (?)
+\item Custom toplevel builder (\texttt{coqmktop}): Jean-Christophe Filliâtre (?)
+\end{itemize}
+
+\section{Graphical interfaces}
+
+\begin{itemize}
+\item Support for {\em PCoq}: Yves Bertot with contributions by
+  Laurence Rideau and Loïc Pottier; additional support for {\em TmEgg}
+  by Lionel Mamane
+\item Support for {\em Proof General}: Pierre Courtieu
+\item {\em CoqIDE}: Benjamin Monate with contributions from
+  Jean-Christophe Filliâtre, Claude Marché, Pierre Letouzey, Julien
+  Narboux, Hugo Herbelin, Pierre Corbineau; uses the Cameleon library
+  by Maxence Guesdon
+\end{itemize}
+
+\section{Architecture}
+
+\begin{itemize}
+\item Functional-kernel-based architecture: Jean-Christophe Filliâtre
+\item Extensible objects and summaries: Chet Murthy
+\item Hash-consing: Bruno Barras
+\item Error locations: Jean-Christophe Filliâtre, Bruno Barras, Hugo Herbelin
+\item Existential variables engine: Chet Murthy with a revision by
+  Bruno Barras and extensions by Clément Renard and Hugo Herbelin
+\end{itemize}
+
+\section{Development tools}
+
+\begin{itemize}
+\item Makefile's: Chet Murthy, Jean-Christophe Filliâtre, Judicaël
+  Courant, Lionel Mamane, Pierre Corbineau, Pierre Letouzey
+\item Debugging: Jean-Christophe Filliâtre with contributions from Jacek Chrz\k{a}szcz, Hugo Herbelin, Bruno Barras, ...
+\item ML quotations: David Delahaye and Daniel de Rauglaudre
+\item ML tactic and vernacular extensions: Hugo Herbelin (first version by Chet Murthy)
+\item Test suite: collective content, initiated by Jean-Christophe Filliâtre with further extensions by Hugo Herbelin, Jean-Marc Notin
+\end{itemize}
+
+\section{Documentation}
+
+\begin{itemize}
+
+\item Reference Manual: collective, layout by Patrick Loiseleur,
+  Claude Marché (former User's Guide in 1991 by Gilles Dowek, Amy
+  Felty, Hugo Herbelin, Gérard Huet, Christine Paulin, Benjamin
+  Werner; initial documentation in 1989 by Thierry Coquand, Gilles
+  Dowek, Gérard Huet, Christine Paulin),
+\item Basic tutorial: Gérard Huet, Gilles Kahn, Christine Paulin
+\item Tutorial on recursive types: Eduardo Gimenez with updates by Pierre Castéran
+\item FAQ: Hugo Herbelin, Julien Narboux, Florent Kirchner
+\end{itemize}
+
+\section{Features discontinued by lack of support}
+
+\begin{itemize}
+\item Searching modulo isomorphism: David Delahaye
+\item Explanation of proofs in pseudo-natural language: Yann Coscoy
+\end{itemize}
+
+Errors may have been inopportunely introduced, please report them to Hugo~\verb=.=~Herbelin~\verb=@=~inria~\verb=.=~fr
+
+\end{document}
diff --git a/doc/whodidwhat/whodidwhat-8.3update.tex b/doc/whodidwhat/whodidwhat-8.3update.tex
new file mode 100644
index 00000000..0a073781
--- /dev/null
+++ b/doc/whodidwhat/whodidwhat-8.3update.tex
@@ -0,0 +1,312 @@
+\documentclass{article}
+
+\usepackage{fullpage}
+\usepackage[utf8]{inputenc}
+\usepackage{t1enc}
+
+\begin{document}
+
+\title{Who did what in the Coq archive?}
+
+\author{The Coq development team}
+
+\maketitle
+
+\centerline{(updated for Coq 8.3)}
+
+\section{The Calculus of Inductive Constructions}
+
+\begin{itemize}
+\item The Calculus of Constructions
+  \begin{itemize}
+  \item Core type-checker: Gérard Huet and Thierry Coquand with
+    optimizations by Chet Murthy, Bruno Barras
+  \item Head reduction functions: Gérard Huet, Christine Paulin, Bruno Barras
+  \end{itemize}
+\item Conversion and reduction
+  \begin{itemize}
+  \item Lazy conversion machine: Bruno Barras
+  \item Transparency/opacity: Bruno Barras
+  \item Bytecode-based conversion: Benjamin Grégoire
+  \item Binary-words retroknowledge: Arnaud Spiwack 
+  \end{itemize}
+\item The universe hierarchy
+  \begin{itemize}
+  \item Floating universes: Gérard Huet, with contributions from Bruno Barras
+  \item Algebraic universes: Hugo Herbelin
+  \end{itemize}
+\item Mutual inductive types and recursive definitions
+  \begin{itemize}
+  \item Type-checking: Christine Paulin
+  \item Positivity condition: Christine Paulin
+  \item Guardness condition for fixpoints: Christine Paulin;
+    extensions by Eduardo Gimenez and Bruno Barras
+  \item Recursively non-uniform parameters: Christine Paulin
+  \item Sort-polymorphism of inductive types: Hugo Herbelin
+  \end{itemize}
+\item Local definitions: Hugo Herbelin
+\item Mutual coinductive types and corecursive definitions: Eduardo Gimenez
+\item Module system
+  \begin{itemize}
+  \item Core system: Jacek Chrz\k{a}szcz
+  \item Inlining: Claudio Sacerdoti Coen and Élie Soubiran
+  \item Module inclusion: Élie Soubiran
+  \item Functorial signature application: Élie Soubiran
+  \item Transparent name space: Élie Soubiran
+  \item Resolution of qualified names: Hugo Herbelin
+  \item Operator for nested functor application: Élie Soubiran and
+    Pierre Letouzey
+  \end{itemize}
+\item Minimalist stand-alone type-checker (\texttt{coqchk}): Bruno Barras, with extra support for modules by Élie Soubiran
+\end{itemize}
+
+\section{Specification language}
+
+\begin{itemize}
+\item Sections: Gilles Dowek with extra contributions by Gérard
+  Huet, Chet Murthy, Hugo Herbelin
+\item The \texttt{Russell} specifications language, proof obligations (\texttt{Program}): Matthieu Sozeau
+\item Type inference: Chet Murthy, with extra contributions by Bruno
+  Barras, Hugo Herbelin and Matthieu Sozeau
+\item Pattern-matching: Hugo Herbelin on top of a first version by
+  Cristina Cornes
+\item Implicit arguments: Amokrane Saïbi, with extensions by Hugo
+  Herbelin and Matthieu Sozeau
+\item Coercions: Amokrane Saïbi
+\item Records: Amokrane Saïbi with extensions by Arnaud Spiwack and
+  Matthieu Sozeau
+\item Canonical structures: Amokrane Saïbi
+\item Type classes: Matthieu Sozeau
+\item Functional schemes (\texttt{Function}, \texttt{Functional Scheme}, ...): Julien Forest and Pierre Courtieu (preliminary version by Yves Bertot)
+\item Generation of induction schemes: Christine Paulin, Vincent
+  Siles, Matthieu Sozeau
+ \end{itemize}
+
+\section{Tactics}
+
+\subsection{General tactic support}
+
+\begin{itemize}
+\item Proof engine: Chet Murthy (first version by Thierry Coquand)
+\item Ltac: David Delahaye, with extensions by Hugo Herbelin, Bruno Barras, ...
+\item Tactic notations: Hugo Herbelin (first version by Chet Murthy)
+\item Main tactic unification procedure: Chet Murthy with
+  contributions from Hugo Herbelin and Matthieu Sozeau
+\item Mathematical-style language (C-Zar): Pierre Corbineau
+\item Communication with external tools (\texttt{external}): Hugo Herbelin
+
+\end{itemize}
+
+\subsection{Predefined tactics}
+
+\begin{itemize}
+\item Basic tactics (\texttt{intro}, \texttt{apply},
+  \texttt{assumption}, \texttt{exact}): Thierry Coquand, with further
+  collective extensions
+\item Reduction tactics: Christine Paulin (\texttt{simpl}), Bruno
+  Barras (\texttt{cbv}, \texttt{lazy}), ...
+\item Tacticals: Thierry Coquand, Chet Murthy, Eduardo Gimenez, ...
+\item Induction: Christine Paulin (\texttt{elim}, \texttt{case}), Hugo Herbelin (\texttt{induction}, \texttt{destruct}, {\tt e}-variants of them), Matthieu Sozeau ({\tt dependent destruction}, {\tt dependent induction})
+\item Refinement (\texttt{refine}): Jean-Christophe Filliâtre
+\item Introduction patterns: Eduardo Gimenez with collective extensions
+\item Forward reasoning: Hugo Herbelin (\texttt{assert}, \texttt{apply in}), Pierre Letouzey (\texttt{specialize}, initial version by Amy Felty)
+\item Rewriting tactics (\texttt{rewrite}): basic version by Christine Paulin,
+  extensions by Jean-Christophe Filliâtre ({\tt subst}), Pierre Letouzey (\verb=!=, \verb=?= modifiers) and Matthieu Sozeau (\verb=*=)
+\item Tactics about equivalence properties (\texttt{reflexivity},
+  \texttt{symmetry}, \texttt{transitivity}): Christine Paulin (?),
+  {\tt e}-variants by Hugo Herbelin, type-classes-based generalization to
+  arbitrary appropriate relations by Matthieu Sozeau
+\item Equality tactics (\texttt{injection}/\texttt{discriminate}):
+  Cristina Cornes
+\item Inversion tactics (\texttt{inversion}): Cristina Cornes, Chet Murthy
+\item Setoid rewriting: Matthieu Sozeau (first version by Clément
+  Renard, second version by Claudio Sacerdoti Coen), contributions
+  from Nicolas Tabareau
+\item Decision of equality: Eduardo Gimenez
+\item Basic Ltac-level tactics: Pierre Letouzey, Matthieu Sozeau,
+  Evgeny Makarov, Hugo Herbelin
+\end{itemize}
+
+\subsection{General automation tactics}
+
+\begin{itemize}
+\item Resolution (\texttt{auto}, \texttt{trivial}): Christine Paulin
+  with extensions from Chet Murthy, Eduardo Gimenez, Patrick
+  Loiseleur (hint bases), Matthieu Sozeau
+\item Resolution with existential variables (\texttt{eauto}): Chet Murthy, Jean-Christophe Filliâtre, with extensions from Matthieu Sozeau
+\item Automatic rewriting (\texttt{autorewrite}): David Delahaye
+\end{itemize}
+
+\subsection{Domain-specific decision tactics}
+
+\begin{itemize}
+\item Congruence closure (\texttt{cc}): Pierre Corbineau
+\item Decision of first-order logic (\texttt{firstorder}): Pierre Corbineau
+\item Simplification of polynomial fractions (\texttt{field}): Laurent
+  Théry and Benjamin Grégoire (first version by David Delahaye and
+  Micaela Mayero)
+\item Simplification of polynomial expressions (\texttt{ring}): Assia
+  Mahboubi, Bruno Barras and Benjamin Grégoire (first version by
+  Samuel Boutin, second version by Patrick Loiseleur)
+\item Decision of systems of polynomial equations: Loïc Pottier (\texttt{nsatz})
+\item Decision of systems of linear inequations: Frédéric Besson
+  (\texttt{psatzl}); Loïc Pottier (\texttt{fourier})
+\item Decision of systems of linear inequations over integers:
+  Frédéric Besson (\texttt{lia}); Pierre Crégut (\texttt{omega} and
+  \texttt{romega})
+\item (Partial) decision of systems of polynomical inequations
+  (\texttt{sos}, \texttt{psatz}): Frédéric Besson, with generalization
+  over arbitrary rings by Evgeny Makarov; uses HOL-Light interface to
+  \texttt{csdp} by John Harrisson
+\item Decision/simplification of intuitionistic propositional logic:
+  David Delahaye (\texttt{tauto}, \texttt{intuition}, first version by
+  Cesar Mu\~noz, second version by Chet Murthy), with contributions
+  from Judicaël Courant; Pierre Corbineau (\texttt{rtauto})
+\item Decision/simplification of intuition first-order logic: Pierre
+  Corbineau (\texttt{firstorder})
+\item Reification ({\tt quote}): Patrick Loiseleur, with
+  generalization by Stéphane Glondu
+\end{itemize}
+
+\section{Extra tools}
+
+\begin{itemize}
+\item Program extraction: Pierre Letouzey (first implementation by
+  Benjamin Werner, second by Jean-Christophe Filliâtre)
+\item Export of context to external communication tools (\texttt{dp}):
+  Nicolas Ayache and Jean-Christophe Filliâtre, with contributions by
+  Claude Marché
+\item Export of terms and environments to XML format: Claudio
+  Sacerdoti Coen, with extensions from Cezary Kaliszyk
+\end{itemize}
+
+\section{Environment management}
+
+\begin{itemize}
+\item Separate compilation: initiated by Chet Murthy
+\item Import/Export: initiated by Chet Murthy
+\item Options management: Hugo Herbelin with contributions by Arnaud Spiwack
+\item Resetting and backtracking: Chet Murthy with contributions from Pierre Courtieu
+\item Searching: Hugo Herbelin and Yves Bertot with extensions by Matthias Puech
+\item Whelp suppport: Hugo Herbelin
+\end{itemize}
+
+\section{Parsing and printing}
+
+\begin{itemize}
+\item General parsing support: Chet Murthy, Bruno Barras, Daniel de Rauglaudre
+\item General printing support: Chet Murthy, Jean-Christophe Filliâtre
+\item Lexing: Daniel de Rauglaudre
+\item Support for UTF-8: Hugo Herbelin, with contributions from Alexandre Miquel and Yann Régis-Gianas
+\item Numerical notations: Hugo Herbelin, Patrick Loiseleur, Micaela Mayero
+\item String notations: Hugo Herbelin
+\item New ``V8'' syntax: Bruno Barras, Hugo Herbelin with contributions by Olivier Desmettre
+\item Abbreviations: Chet Murthy
+\item Notations: Chet Murthy, Hugo Herbelin
+\end{itemize}
+
+\section{Libraries}
+
+\begin{itemize}
+\item Init: collective (initiated by Christine Paulin and Gérard Huet)
+\item Arith: collective (initiated by Christine Paulin)
+\item ZArith: collective (initiated by Pierre Crégut)
+\item Bool: collective (initiated by Christine Paulin)
+\item NArith: Hugo Herbelin, Pierre Letouzey, Evgeny Makarov (out of
+  initial contibution by Pierre Crégut)
+\item Lists: Pierre Letouzey, Jean-Marc Notin (initiated by Christine Paulin)
+\item Reals: Micaela Mayero (axiomatization and main properties), Olivier Desmettre (convergence, derivability, integrals, trigonometric functions), contributions from Russell O'Connor, Cezary Kaliszyk, Guillaume Melquiond
+\item Relations: Bruno Barras, Cristina Cornes with contributions from
+  Pierre Castéran
+\item Wellfounded: Bruno Barras, Cristina Cornes
+\item FSets: Pierre Letouzey, from initial work with Jean-Christophe Filliâtre, decision tactic for FSets by Aaron Bohannon
+\item MSets: Pierre Letouzey
+\item Logic: Christine Paulin, Hugo Herbelin, Bruno Barras
+\item Numbers: Evgeny Makarov (abstractions), Laurent Théry and Benjamin Grégoire (big numbers), Arnaud Spiwack and Pierre Letouzey (word-based arithmetic), further extensions by Pierre Letouzey
+\item Classes: Matthieu Sozeau
+\item QArith: Pierre Letouzey, with contributions from Russell O'Connor
+\item Setoid: Matthieu Sozeau (first version by Clément Renard, second version by Claudio Sacerdoti Coen)
+\item Sets: Gilles Kahn and Gérard Huet
+\item Sorting: Gérard Huet with revisions by Hugo Herbelin
+\item Strings: Laurent Théry
+\item Program: Matthieu Sozeau
+\item Unicode: Claude Marché
+\end{itemize}
+
+\section{Commands}
+
+\begin{itemize}
+\item Batch compiler (\texttt{coqc}):  Chet Murthy (?)
+\item Compilation dependency calculator (\texttt{coqdep}):
+  Jean-Christophe Filliâtre
+\item Statistic tool (\texttt{coqwc}): Jean-Christophe Filliâtre
+\item Simple html presentation tool (\texttt{gallina}) (deprecated): Jean-Christophe Filliâtre
+\item Auto-maker (\texttt{coq\_makefile}): Jean-Christophe Filliâtre,
+  with contributions from Judicaël Courant
+\item LaTeX presentation tool (\texttt{coq-tex}): Jean-Christophe Filliâtre
+\item Multi-purpose presentation tool (\texttt{coqdoc}): Jean-Christophe Filliâtre with extensions from
+  Matthieu Sozeau, Jean-Marc Notin, Hugo Herbelin
+\item Interactive toplevel (\texttt{coqtop}): Jean-Christophe Filliâtre (?)
+\item Custom toplevel builder (\texttt{coqmktop}): Jean-Christophe Filliâtre (?)
+\end{itemize}
+
+\section{Graphical interfaces}
+
+\begin{itemize}
+\item Support for {\em PCoq}: Yves Bertot with contributions by
+  Laurence Rideau and Loïc Pottier; additional support for {\em TmEgg}
+  by Lionel Mamane
+\item Support for {\em Proof General}: Pierre Courtieu
+\item {\em CoqIDE}: Benjamin Monate with contributions from
+  Jean-Christophe Filliâtre, Claude Marché, Pierre Letouzey, Julien
+  Narboux, Hugo Herbelin, Pierre Corbineau, Vincent Gross; uses the Cameleon library
+  by Maxence Guesdon
+\end{itemize}
+
+\section{Architecture}
+
+\begin{itemize}
+\item Functional-kernel-based architecture: Jean-Christophe Filliâtre
+\item Extensible objects and summaries: Chet Murthy
+\item Hash-consing: Bruno Barras
+\item Error locations: Jean-Christophe Filliâtre, Bruno Barras, Hugo Herbelin
+\item Existential variables engine: Chet Murthy with revisions by
+  Bruno Barras and Arnaud Spiwack and extensions by Clément Renard and
+  Hugo Herbelin
+\end{itemize}
+
+\section{Development tools}
+
+\begin{itemize}
+\item Makefile's: Chet Murthy, Jean-Christophe Filliâtre, Judicaël
+  Courant, Lionel Mamane, Pierre Corbineau, Pierre Letouzey
+\item Debugging: Jean-Christophe Filliâtre with contributions from Jacek Chrz\k{a}szcz, Hugo Herbelin, Bruno Barras, ...
+\item ML quotations: David Delahaye and Daniel de Rauglaudre
+\item ML tactic and vernacular extensions: Hugo Herbelin (first version by Chet Murthy)
+\item Test suite: collective content, initiated by Jean-Christophe Filliâtre with further extensions by Hugo Herbelin, Jean-Marc Notin
+\end{itemize}
+
+\section{Documentation}
+
+\begin{itemize}
+
+\item Reference Manual: collective, layout by Patrick Loiseleur,
+  Claude Marché (former User's Guide in 1991 by Gilles Dowek, Amy
+  Felty, Hugo Herbelin, Gérard Huet, Christine Paulin, Benjamin
+  Werner; initial documentation in 1989 by Thierry Coquand, Gilles
+  Dowek, Gérard Huet, Christine Paulin),
+\item Basic tutorial: Gérard Huet, Gilles Kahn, Christine Paulin
+\item Tutorial on recursive types: Eduardo Gimenez with updates by Pierre Castéran
+\item FAQ: Hugo Herbelin, Julien Narboux, Florent Kirchner
+\end{itemize}
+
+\section{Features discontinued by lack of support}
+
+\begin{itemize}
+\item Searching modulo isomorphism: David Delahaye
+\item Explanation of proofs in pseudo-natural language: Yann Coscoy
+\end{itemize}
+
+Errors may have been inopportunely introduced, please report them to Hugo~\verb=.=~Herbelin~\verb=@=~inria~\verb=.=~fr
+
+\end{document}
diff --git a/doc/whodidwhat/whodidwhat-8.4update.tex b/doc/whodidwhat/whodidwhat-8.4update.tex
new file mode 100644
index 00000000..696fff4f
--- /dev/null
+++ b/doc/whodidwhat/whodidwhat-8.4update.tex
@@ -0,0 +1,334 @@
+\documentclass{article}
+
+\usepackage{fullpage}
+\usepackage[utf8]{inputenc}
+\usepackage{t1enc}
+
+\begin{document}
+
+\title{Who did what in the Coq archive?}
+
+\author{The Coq development team}
+
+\maketitle
+
+\centerline{(updated for Coq 8.4)}
+
+\section{The Calculus of Inductive Constructions}
+
+\begin{itemize}
+\item The Calculus of Constructions
+  \begin{itemize}
+  \item Core type-checker: Gérard Huet and Thierry Coquand with
+    optimizations by Chet Murthy, Bruno Barras
+  \item Head reduction functions: Gérard Huet, Christine Paulin, Bruno Barras
+  \end{itemize}
+\item Conversion and reduction
+  \begin{itemize}
+  \item Lazy conversion machine: Bruno Barras
+  \item Transparency/opacity: Bruno Barras
+  \item Bytecode-based conversion: Benjamin Grégoire
+  \item Binary-words retroknowledge: Arnaud Spiwack 
+  \end{itemize}
+\item The universe hierarchy
+  \begin{itemize}
+  \item Floating universes: Gérard Huet, with contributions from Bruno Barras
+  \item Algebraic universes: Hugo Herbelin
+  \end{itemize}
+\item Mutual inductive types and recursive definitions
+  \begin{itemize}
+  \item Type-checking: Christine Paulin
+  \item Positivity condition: Christine Paulin
+  \item Guardness condition for fixpoints: Christine Paulin;
+    extensions by Eduardo Gimenez, Bruno Barras, Pierre Boutillier
+  \item Recursively non-uniform parameters: Christine Paulin
+  \item Sort-polymorphism of inductive types: Hugo Herbelin
+  \end{itemize}
+\item Local definitions: Hugo Herbelin
+\item Mutual coinductive types and corecursive definitions: Eduardo Gimenez
+\item Module system
+  \begin{itemize}
+  \item Core system: Jacek Chrz\k{a}szcz
+  \item Inlining: Claudio Sacerdoti Coen and Élie Soubiran
+  \item Module inclusion: Élie Soubiran
+  \item Functorial signature application: Élie Soubiran
+  \item Transparent name space: Élie Soubiran
+  \item Resolution of qualified names: Hugo Herbelin
+  \item Operator for nested functor application: Élie Soubiran and
+    Pierre Letouzey
+  \end{itemize}
+\item Minimalist stand-alone type-checker (\texttt{coqchk}): Bruno Barras, with extra support for modules by Élie Soubiran and Pierre Letouzey
+\item Eta-conversion: Hugo Herbelin, with contributions from Stéphane
+  Glondu, Benjamin Grégoire
+\end{itemize}
+
+\section{Specification language}
+
+\begin{itemize}
+\item Sections: Gilles Dowek with extra contributions by Gérard
+  Huet, Chet Murthy, Hugo Herbelin
+\item The \texttt{Russell} specifications language, proof obligations (\texttt{Program}): Matthieu Sozeau
+\item Type inference: Chet Murthy, with extra contributions by Bruno
+  Barras, Hugo Herbelin, Matthieu Sozeau, Enrico Tassi
+\item Pattern-matching: Hugo Herbelin on top of a first version by
+  Cristina Cornes
+\item Implicit arguments: Amokrane Saïbi, with extensions by Hugo
+  Herbelin, Matthieu Sozeau, Pierre Boutillier
+\item Synthetic {\tt Arguments} command: Enrico Tassi
+\item Coercions: Amokrane Saïbi
+\item Records: Amokrane Saïbi with extensions by Arnaud Spiwack and
+  Matthieu Sozeau
+\item Canonical structures: Amokrane Saïbi
+\item Type classes: Matthieu Sozeau
+\item Functional schemes (\texttt{Function}, \texttt{Functional Scheme}, ...): Julien Forest and Pierre Courtieu (preliminary version by Yves Bertot)
+\item Generation of induction schemes: Christine Paulin, Vincent
+  Siles, Matthieu Sozeau
+ \end{itemize}
+
+\section{Tactics}
+
+\subsection{General tactic support}
+
+\begin{itemize}
+\item Proof engine: Arnaud Spiwack (first version by Thierry Coquand, second version by Chet Murthy)
+\item Ltac: David Delahaye, with extensions by Hugo Herbelin, Bruno Barras, ...
+\item Tactic notations: Hugo Herbelin (first version by Chet Murthy)
+\item Main tactic unification procedure: Chet Murthy with
+  contributions from Hugo Herbelin and Matthieu Sozeau
+\item Mathematical-style language (C-Zar): Pierre Corbineau
+\item Communication with external tools (\texttt{external}): Hugo Herbelin
+\item Proof structuring (bullets and brackets): Arnaud Spiwack
+\end{itemize}
+
+\subsection{Predefined tactics}
+
+\begin{itemize}
+\item Basic tactics (\texttt{intro}, \texttt{apply},
+  \texttt{assumption}, \texttt{exact}): Thierry Coquand, with further
+  collective extensions
+\item Reduction tactics: Christine Paulin (\texttt{simpl}), Bruno
+  Barras (\texttt{cbv}, \texttt{lazy}), with contributions from Hugo Herbelin, Enrico Tassi, ...
+\item Tacticals: Thierry Coquand, Chet Murthy, Eduardo Gimenez, ...;
+  new versions of {\tt info} and {\tt Show Script} by Pierre Letouzey;
+  {\tt timeout} by Pierre Letouzey
+\item Induction: Christine Paulin (\texttt{elim}, \texttt{case}), Hugo Herbelin (\texttt{induction}, \texttt{destruct}
+\item Refinement (\texttt{refine}): Jean-Christophe Filliâtre
+\item Introduction patterns: Eduardo Gimenez with collective extensions
+\item Forward reasoning: Hugo Herbelin (\texttt{assert}, \texttt{apply in}), Pierre Letouzey (\texttt{specialize}, initial version by Amy Felty)
+\item Rewriting tactics (\texttt{rewrite}): basic version by Christine Paulin,
+  extensions by Jean-Christophe Filliâtre and Pierre Letouzey
+\item Tactics about equivalence properties (\texttt{reflexivity},
+  \texttt{symmetry}, \texttt{transitivity}): Christine Paulin (?),
+\item Equality tactics (\texttt{injection}/\texttt{discriminate}):
+  Cristina Cornes
+\item Inversion tactics (\texttt{inversion}): Cristina Cornes, Chet Murthy
+\item Setoid rewriting: Matthieu Sozeau (first version by Clément
+  Renard, second version by Claudio Sacerdoti Coen), contributions
+  from Nicolas Tabareau
+\item Decision of equality: Eduardo Gimenez
+\item Basic Ltac-level tactics: Pierre Letouzey, Matthieu Sozeau,
+  Evgeny Makarov
+\item Tactics about existential variables: Clément Renard, Pierre Corbineau, Stéphane Glondu, Arnaud Spiwack, ...
+\end{itemize}
+
+\subsection{General automation tactics}
+
+\begin{itemize}
+\item Resolution (\texttt{auto}, \texttt{trivial}): Christine Paulin
+  with extensions from Chet Murthy, Eduardo Gimenez, Patrick
+  Loiseleur (hint bases), Matthieu Sozeau
+\item Resolution with existential variables (\texttt{eauto}): Chet Murthy, Jean-Christophe Filliâtre, with extensions from Matthieu Sozeau
+\item Automatic rewriting (\texttt{autorewrite}): David Delahaye
+\end{itemize}
+
+\subsection{Domain-specific decision tactics}
+
+\begin{itemize}
+\item Congruence closure (\texttt{cc}): Pierre Corbineau
+\item Decision of first-order logic (\texttt{firstorder}): Pierre Corbineau
+\item Simplification of polynomial fractions (\texttt{field}): Laurent
+  Théry and Benjamin Grégoire (first version by David Delahaye and
+  Micaela Mayero)
+\item Simplification of polynomial expressions (\texttt{ring}): Assia
+  Mahboubi, Bruno Barras and Benjamin Grégoire (first version by
+  Samuel Boutin, second version by Patrick Loiseleur)
+\item Decision of systems of polynomial equations: Loïc Pottier (\texttt{nsatz})
+\item Decision of systems of linear inequations: Frédéric Besson
+  (\texttt{psatzl}); Loïc Pottier (\texttt{fourier})
+\item Decision of systems of linear inequations over integers:
+  Frédéric Besson (\texttt{lia}); Pierre Crégut (\texttt{omega} and
+  \texttt{romega})
+\item (Partial) decision of systems of polynomical inequations
+  (\texttt{sos}, \texttt{psatz}): Frédéric Besson, with generalization
+  over arbitrary rings by Evgeny Makarov; uses HOL-Light interface to
+  \texttt{csdp} by John Harrisson
+\item Decision/simplification of intuitionistic propositional logic:
+  David Delahaye (\texttt{tauto}, \texttt{intuition}, first version by
+  Cesar Mu\~noz, second version by Chet Murthy), with contributions
+  from Judicaël Courant; Pierre Corbineau (\texttt{rtauto})
+\item Decision/simplification of intuition first-order logic: Pierre
+  Corbineau (\texttt{firstorder})
+\end{itemize}
+
+\section{Extra tools}
+
+\begin{itemize}
+\item Program extraction: Pierre Letouzey (first implementation by
+  Benjamin Werner, second by Jean-Christophe Filliâtre)
+\item Export of context to external communication tools (\texttt{dp}):
+  Nicolas Ayache and Jean-Christophe Filliâtre, with contributions by
+  Claude Marché
+\item Export of terms and environments to XML format: Claudio
+  Sacerdoti Coen, with extensions from Cezary Kaliszyk
+\end{itemize}
+
+\section{Environment management}
+
+\begin{itemize}
+\item Separate compilation: initiated by Chet Murthy
+\item Import/Export: initiated by Chet Murthy
+\item Options management: Hugo Herbelin with contributions by Arnaud Spiwack
+\item Resetting and backtracking: Chet Murthy with contributions from Pierre Courtieu
+\item Searching: Hugo Herbelin and Yves Bertot with extensions by Matthias Puech
+\item Whelp suppport: Hugo Herbelin
+\end{itemize}
+
+\section{Parsing and printing}
+
+\begin{itemize}
+\item General parsing support: Chet Murthy, Bruno Barras, Daniel de Rauglaudre
+\item General printing support: Chet Murthy, Jean-Christophe Filliâtre
+\item Lexing: Daniel de Rauglaudre
+\item Support for UTF-8: Hugo Herbelin, with contributions from Alexandre Miquel and Yann Régis-Gianas
+\item Numerical notations: Hugo Herbelin, Patrick Loiseleur, Micaela Mayero
+\item String notations: Hugo Herbelin
+\item New ``V8'' syntax: Bruno Barras, Hugo Herbelin with contributions by Olivier Desmettre
+\item Abbreviations: Chet Murthy
+\item Notations: Chet Murthy, Hugo Herbelin
+\end{itemize}
+
+\section{Libraries}
+
+\begin{itemize}
+\item Init: collective (initiated by Christine Paulin and Gérard Huet)
+\item Arith: collective (initiated by Christine Paulin)
+\item ZArith: collective (initiated by Pierre Crégut)
+\item Bool: collective (initiated by Christine Paulin)
+\item NArith: Hugo Herbelin, Pierre Letouzey, Evgeny Makarov (out of
+  initial contibution by Pierre Crégut)
+\item Lists: Pierre Letouzey, Jean-Marc Notin (initiated by Christine Paulin)
+\item Vectors: Pierre Boutillier
+\item Reals: Micaela Mayero (axiomatization and main properties), Olivier Desmettre (convergence, derivability, integrals, trigonometric functions), contributions from Russell O'Connor, Cezary Kaliszyk, Guillaume Melquiond, Yves Bertot, Guillaume Allais
+\item Relations: Bruno Barras, Cristina Cornes with contributions from
+  Pierre Castéran
+\item Wellfounded: Bruno Barras, Cristina Cornes
+\item FSets: Pierre Letouzey, from initial work with Jean-Christophe Filliâtre, decision tactic for FSets by Aaron Bohannon, red-black trees by Andrew Appel and Pierre Letouzey
+\item MSets: Pierre Letouzey
+\item Logic: Christine Paulin, Hugo Herbelin, Bruno Barras
+\item Numbers: Evgeny Makarov (abstractions), Laurent Théry and Benjamin Grégoire (big numbers), Arnaud Spiwack and Pierre Letouzey (word-based arithmetic), further extensions by Pierre Letouzey; integration of Arith and ZArith to Numbers by Pierre Letouzey
+\item Classes: Matthieu Sozeau
+\item QArith: Pierre Letouzey, with contributions from Russell O'Connor
+\item Setoid: Matthieu Sozeau (first version by Clément Renard, second version by Claudio Sacerdoti Coen)
+\item Sets: Gilles Kahn and Gérard Huet
+\item Sorting: Gérard Huet with revisions by Hugo Herbelin
+\item Strings: Laurent Théry
+\item Program: Matthieu Sozeau
+\item Unicode: Claude Marché
+\end{itemize}
+
+\section{Commands}
+
+\begin{itemize}
+\item Batch compiler (\texttt{coqc}):  Chet Murthy (?)
+\item Compilation dependency calculator (\texttt{coqdep}):
+  Jean-Christophe Filliâtre
+\item Statistic tool (\texttt{coqwc}): Jean-Christophe Filliâtre
+\item Simple html presentation tool (\texttt{gallina}) (deprecated): Jean-Christophe Filliâtre
+\item Auto-maker (\texttt{coq\_makefile}): Jean-Christophe Filliâtre,
+  with contributions from Judicaël Courant, updated by Pierre Boutillier
+\item LaTeX presentation tool (\texttt{coq-tex}): Jean-Christophe Filliâtre
+\item Multi-purpose presentation tool (\texttt{coqdoc}): Jean-Christophe Filliâtre with extensions from
+  Matthieu Sozeau, Jean-Marc Notin, Hugo Herbelin and contributions from Adam Chlipala
+\item Interactive toplevel (\texttt{coqtop}): Jean-Christophe Filliâtre (?)
+\item Custom toplevel builder (\texttt{coqmktop}): Jean-Christophe Filliâtre (?)
+\end{itemize}
+
+\section{Graphical interfaces}
+
+\begin{itemize}
+\item Support for {\em PCoq}: Yves Bertot with contributions by
+  Laurence Rideau and Loïc Pottier; additional support for {\em TmEgg}
+  by Lionel Mamane
+\item Support for {\em Proof General}: Pierre Courtieu with contributions from Arnaud Spiwack
+\item {\em CoqIDE}: Benjamin Monate with contributions from
+  Jean-Christophe Filliâtre, Claude Marché, Pierre Letouzey, Julien
+  Narboux, Hugo Herbelin, Pierre Corbineau, Pierre Boutillier,
+  Pierre-Marie Pédrot; processus-based communication protocol by
+  Vincent Gross with contributions from Pierre Letouzey, Pierre
+  Boutillier, Pierre-Marie Pédrot; backtracking revised by Pierre
+  Letouzey; uses the Cameleon library by Maxence Guesdon;
+\end{itemize}
+
+\section{Architecture}
+
+\begin{itemize}
+\item Functional-kernel-based architecture: Jean-Christophe Filliâtre
+\item Extensible objects and summaries: Chet Murthy
+\item Hash-consing: Bruno Barras
+\item Error locations: Jean-Christophe Filliâtre, Bruno Barras, Hugo Herbelin, with contributions from Arnaud Spiwack
+\item Existential variables engine: Chet Murthy with revisions by
+  Bruno Barras and Arnaud Spiwack and extensions by Clément Renard and
+  Hugo Herbelin
+\end{itemize}
+
+\section{Development tools}
+
+\begin{itemize}
+\item Makefile's: Chet Murthy, Jean-Christophe Filliâtre, Judicaël
+  Courant, Lionel Mamane, Pierre Corbineau, Pierre Letouzey with
+  contributions from Stéphane Glondu, Hugo Herbelin, ...
+\item Debugging: Jean-Christophe Filliâtre with contributions from Jacek Chrz\k{a}szcz, Hugo Herbelin, Bruno Barras, ...
+\item ML quotations: David Delahaye and Daniel de Rauglaudre
+\item ML tactic and vernacular extensions: Hugo Herbelin (first version by Chet Murthy)
+\item Test suite: collective content, initiated by Jean-Christophe Filliâtre with further extensions by Hugo Herbelin, Jean-Marc Notin
+\end{itemize}
+
+\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 Team coordination: Gérard Huet, Christine Paulin, Hugo Herbelin,
+  with various other contributions
+\item Packaging tools: Henri Laulhere, David Delahaye, Julien Narboux,
+  Pierre Letouzey, Enrico Tassi (Windows); Damien Doligez, Hugo
+  Herbelin, Pierre Boutillier (MacOS); Jean-Christophe Filliâtre,
+  Judicaël Courant, Hugo Herbelin, Stéphane Glondu (Linux)
+\end{itemize}
+
+\section{Documentation}
+
+\begin{itemize}
+
+\item Reference Manual: collective, layout by Patrick Loiseleur,
+  Claude Marché (former User's Guide in 1991 by Gilles Dowek, Amy
+  Felty, Hugo Herbelin, Gérard Huet, Christine Paulin, Benjamin
+  Werner; initial documentation in 1989 by Thierry Coquand, Gilles
+  Dowek, Gérard Huet, Christine Paulin),
+\item Basic tutorial: Gérard Huet, Gilles Kahn, Christine Paulin
+\item Tutorial on recursive types: Eduardo Gimenez with updates by Pierre Castéran
+\item FAQ: Hugo Herbelin, Julien Narboux, Florent Kirchner
+\end{itemize}
+
+\section{Features discontinued by lack of support}
+
+\begin{itemize}
+\item Searching modulo isomorphism: David Delahaye
+\item Explanation of proofs in pseudo-natural language: Yann Coscoy
+\end{itemize}
+
+For probable oversights or accidental errors, please report to Hugo~\verb=.=~Herbelin~\verb=@=~inria~\verb=.=~fr
+
+\end{document}
diff --git a/doc/whodidwhat/whodidwhat-8.5update.tex b/doc/whodidwhat/whodidwhat-8.5update.tex
new file mode 100644
index 00000000..ce099dc3
--- /dev/null
+++ b/doc/whodidwhat/whodidwhat-8.5update.tex
@@ -0,0 +1,346 @@
+\documentclass{article}
+
+\usepackage{fullpage}
+\usepackage[utf8]{inputenc}
+\usepackage{t1enc}
+
+\begin{document}
+
+\title{Who did what in the Coq archive?}
+
+\author{The Coq development team}
+
+\maketitle
+
+\centerline{(updated for Coq 8.5)}
+
+\section{The Calculus of Inductive Constructions}
+
+\begin{itemize}
+\item The Calculus of Constructions
+  \begin{itemize}
+  \item Core type-checker: Gérard Huet and Thierry Coquand with
+    optimizations by Chet Murthy, Bruno Barras
+  \item Head reduction functions: Gérard Huet, Christine Paulin, Bruno Barras
+  \end{itemize}
+\item Conversion and reduction
+  \begin{itemize}
+  \item Lazy conversion machine: Bruno Barras
+  \item Transparency/opacity: Bruno Barras
+  \item Bytecode-based conversion: Benjamin Grégoire
+  \item Binary-words retroknowledge: Arnaud Spiwack 
+  \item Native code based conversion: Maxime Dénès, Benjamin Grégoire
+  \end{itemize}
+\item The universe hierarchy
+  \begin{itemize}
+  \item Floating universes: Gérard Huet, with contributions from Bruno Barras
+  \item Algebraic universes: Hugo Herbelin
+  \end{itemize}
+\item Mutual inductive types and recursive definitions
+  \begin{itemize}
+  \item Type-checking: Christine Paulin
+  \item Positivity condition: Christine Paulin
+  \item Guardness condition for fixpoints: Christine Paulin;
+    extensions by Eduardo Gimenez, Bruno Barras, Pierre Boutillier; fixes by
+    Bruno Barras, Maxime Dénès
+  \item Recursively non-uniform parameters: Christine Paulin
+  \item Sort-polymorphism of inductive types: Hugo Herbelin
+  \end{itemize}
+\item Local definitions: Hugo Herbelin
+\item Mutual coinductive types and corecursive definitions: Eduardo Gimenez
+\item Module system
+  \begin{itemize}
+  \item Core system: Jacek Chrz\k{a}szcz
+  \item Inlining: Claudio Sacerdoti Coen and Élie Soubiran
+  \item Module inclusion: Élie Soubiran
+  \item Functorial signature application: Élie Soubiran
+  \item Transparent name space: Élie Soubiran
+  \item Resolution of qualified names: Hugo Herbelin
+  \item Operator for nested functor application: Élie Soubiran and
+    Pierre Letouzey
+  \end{itemize}
+\item Minimalist stand-alone type-checker (\texttt{coqchk}): Bruno Barras, with extra support for modules by Élie Soubiran and Pierre Letouzey
+\item Eta-conversion: Hugo Herbelin, with contributions from Stéphane
+  Glondu, Benjamin Grégoire
+\end{itemize}
+
+\section{Specification language}
+
+\begin{itemize}
+\item Sections: Gilles Dowek with extra contributions by Gérard
+  Huet, Chet Murthy, Hugo Herbelin
+\item The \texttt{Russell} specifications language, proof obligations (\texttt{Program}): Matthieu Sozeau
+\item Type inference: Chet Murthy, with extra contributions by Bruno
+  Barras, Hugo Herbelin, Matthieu Sozeau, Enrico Tassi
+\item Pattern-matching: Hugo Herbelin on top of a first version by
+  Cristina Cornes, contributions by Arnaud Spiwack
+\item Implicit arguments: Amokrane Saïbi, with extensions by Hugo
+  Herbelin, Matthieu Sozeau, Pierre Boutillier
+\item Synthetic {\tt Arguments} command: Enrico Tassi
+\item Coercions: Amokrane Saïbi
+\item Records
+  \begin{itemize}
+  \item Core implementation: Amokrane Saïbi with extensions by Matthieu Sozeau
+  \item Extension to inductive and co-inductive records: Arnaud Spiwack
+  \item Non-recursive variants: Arnaud Spiwack
+  \end{itemize}
+\item Canonical structures: Amokrane Saïbi
+\item Type classes: Matthieu Sozeau
+\item Function (\texttt{Function}, \texttt{functional induction}...):
+  Julien Forest (preliminary versions by Pierre Courtieu
+  (\texttt{Functional Schemes}) and Yves Bertot (\texttt{Recursive
+    Definition}))
+\item Generation of induction schemes: Christine Paulin, Vincent
+  Siles, Matthieu Sozeau
+ \end{itemize}
+
+\section{Tactics}
+
+\subsection{General tactic support}
+
+\begin{itemize}
+\item Proof engine: Arnaud Spiwack (first version by Thierry Coquand, second version by Chet Murthy)
+\item Ltac: David Delahaye, with extensions by Hugo Herbelin, Bruno Barras, ...
+  Evolution to the new proof engine Arnaud Spiwack, Pierre-Marie P\'edrot
+\item Tactic notations: Hugo Herbelin (first version by Chet Murthy)
+\item Main tactic unification procedure: Chet Murthy with
+  contributions from Hugo Herbelin and Matthieu Sozeau
+\item Mathematical-style language (C-Zar): Pierre Corbineau
+\item Communication with external tools (\texttt{external}): Hugo Herbelin
+\item Proof structuring (bullets and brackets): Arnaud Spiwack
+\end{itemize}
+
+\subsection{Predefined tactics}
+
+\begin{itemize}
+\item Basic refinement tactic (\texttt{refine}): Arnaud Spiwack (previous non-basic version by Jean-Christophe Filliâtre)
+\item Core tactics (\texttt{intro}, \texttt{apply},
+  \texttt{assumption}, \texttt{exact}): Thierry Coquand, with further
+  collective extensions
+\item Reduction tactics: Christine Paulin (\texttt{simpl}), Bruno
+  Barras (\texttt{cbv}, \texttt{lazy}), Pierre Boutillier (\texttt{cbn})
+  with contributions from Hugo Herbelin, Enrico Tassi, ...
+\item Tacticals: Thierry Coquand, Chet Murthy, Eduardo Gimenez, ...;
+  new versions of {\tt info} and {\tt Show Script} by Pierre Letouzey;
+  {\tt timeout} by Pierre Letouzey; backtracking-related tacticals by Arnaud Spiwack
+\item Generic tactic traces ({\tt Info}) by Arnaud Spiwack (based on the former {\tt info} tactical)
+\item Induction: Christine Paulin (\texttt{elim}, \texttt{case}), Hugo Herbelin (\texttt{induction}, \texttt{destruct}
+\item Introduction patterns: Eduardo Gimenez with collective extensions
+\item Forward reasoning: Hugo Herbelin (\texttt{assert}, \texttt{enough}, \texttt{apply in}),
+  Pierre Letouzey (\texttt{specialize}, initial version by Amy Felty)
+\item Rewriting tactics (\texttt{rewrite}): basic version by Christine Paulin,
+  extensions by Jean-Christophe Filliâtre and Pierre Letouzey
+\item Setoid rewriting: Matthieu Sozeau (first version by Clément
+  Renard, second version by Claudio Sacerdoti Coen), contributions
+  from Nicolas Tabareau
+\item Tactics about equivalence properties (\texttt{reflexivity},
+  \texttt{symmetry}, \texttt{transitivity}): Christine Paulin (?),
+\item Equality tactics (\texttt{injection}/\texttt{discriminate}): Cristina Cornes, extensions by Hugo Herbelin
+\item Inversion tactics (\texttt{inversion}): Cristina Cornes, Chet Murthy
+\item Decision of equality: Eduardo Gimenez
+\item Basic Ltac-level tactics: Pierre Letouzey, Matthieu Sozeau,
+  Evgeny Makarov
+\item Tactics about existential variables: Clément Renard, Pierre Corbineau, Stéphane Glondu, Arnaud Spiwack, ...
+\end{itemize}
+
+\subsection{General automation tactics}
+
+\begin{itemize}
+\item Resolution (\texttt{auto}, \texttt{trivial}): Christine Paulin
+  with extensions from Chet Murthy, Eduardo Gimenez, Patrick
+  Loiseleur (hint bases), Matthieu Sozeau
+\item Resolution with existential variables (\texttt{eauto}): Chet Murthy, Jean-Christophe Filliâtre, with extensions from Matthieu Sozeau
+\item Automatic rewriting (\texttt{autorewrite}): David Delahaye
+\end{itemize}
+
+\subsection{Domain-specific decision tactics}
+
+\begin{itemize}
+\item Congruence closure (\texttt{cc}): Pierre Corbineau
+\item Decision of first-order logic (\texttt{firstorder}): Pierre Corbineau
+\item Simplification of polynomial fractions (\texttt{field}): Laurent
+  Théry and Benjamin Grégoire (first version by David Delahaye and
+  Micaela Mayero)
+\item Simplification of polynomial expressions (\texttt{ring}): Assia
+  Mahboubi, Bruno Barras and Benjamin Grégoire (first version by
+  Samuel Boutin, second version by Patrick Loiseleur)
+\item Decision of systems of polynomial equations: Loïc Pottier (\texttt{nsatz})
+\item Decision of systems of linear inequations: Frédéric Besson
+  (\texttt{psatzl}); Loïc Pottier (\texttt{fourier})
+\item Decision of systems of linear inequations over integers:
+  Frédéric Besson (\texttt{lia}); Pierre Crégut (\texttt{omega} and
+  \texttt{romega})
+\item (Partial) decision of systems of polynomical inequations
+  (\texttt{sos}, \texttt{psatz}): Frédéric Besson, with generalization
+  over arbitrary rings by Evgeny Makarov; uses HOL-Light interface to
+  \texttt{csdp} by John Harrisson
+\item Decision/simplification of intuitionistic propositional logic:
+  David Delahaye (\texttt{tauto}, \texttt{intuition}, first version by
+  Cesar Mu\~noz, second version by Chet Murthy), with contributions
+  from Judicaël Courant; Pierre Corbineau (\texttt{rtauto})
+\item Decision/simplification of intuition first-order logic: Pierre
+  Corbineau (\texttt{firstorder})
+\end{itemize}
+
+\section{Extra tools}
+
+\begin{itemize}
+\item Program extraction: Pierre Letouzey (first implementation by
+  Benjamin Werner, second by Jean-Christophe Filliâtre)
+\end{itemize}
+
+\section{Environment management}
+
+\begin{itemize}
+\item Separate compilation: initiated by Chet Murthy
+\item Import/Export: initiated by Chet Murthy
+\item Options management: Hugo Herbelin with contributions by Arnaud Spiwack
+\item Resetting and backtracking: Chet Murthy with contributions from Pierre Courtieu
+\item Searching: Hugo Herbelin and Yves Bertot with extensions by Matthias Puech
+\item Whelp suppport: Hugo Herbelin
+\end{itemize}
+
+\section{Parsing and printing}
+
+\begin{itemize}
+\item General parsing support: Chet Murthy, Bruno Barras, Daniel de Rauglaudre
+\item General printing support: Chet Murthy, Jean-Christophe Filliâtre
+\item Lexing: Daniel de Rauglaudre
+\item Support for UTF-8: Hugo Herbelin, with contributions from Alexandre Miquel and Yann Régis-Gianas
+\item Numerical notations: Hugo Herbelin, Patrick Loiseleur, Micaela Mayero
+\item String notations: Hugo Herbelin
+\item New ``V8'' syntax: Bruno Barras, Hugo Herbelin with contributions by Olivier Desmettre
+\item Abbreviations: Chet Murthy
+\item Notations: Chet Murthy, Hugo Herbelin
+\end{itemize}
+
+\section{Libraries}
+
+\begin{itemize}
+\item Init: collective (initiated by Christine Paulin and Gérard Huet)
+\item Arith: collective (initiated by Christine Paulin)
+\item ZArith: collective (initiated by Pierre Crégut)
+\item Bool: collective (initiated by Christine Paulin)
+\item NArith: Hugo Herbelin, Pierre Letouzey, Evgeny Makarov (out of
+  initial contibution by Pierre Crégut)
+\item Lists: Pierre Letouzey, Jean-Marc Notin (initiated by Christine Paulin)
+\item Vectors: Pierre Boutillier
+\item Reals: Micaela Mayero (axiomatization and main properties), Olivier Desmettre (convergence, derivability, integrals, trigonometric functions), contributions from Russell O'Connor, Cezary Kaliszyk, Guillaume Melquiond, Yves Bertot, Guillaume Allais
+\item Relations: Bruno Barras, Cristina Cornes with contributions from
+  Pierre Castéran
+\item Wellfounded: Bruno Barras, Cristina Cornes
+\item FSets: Pierre Letouzey, from initial work with Jean-Christophe Filliâtre, decision tactic for FSets by Aaron Bohannon, red-black trees by Andrew Appel and Pierre Letouzey
+\item MSets: Pierre Letouzey
+\item Logic: Christine Paulin, Hugo Herbelin, Bruno Barras, contributions by Arnaud Spiwack
+\item Numbers: Evgeny Makarov (abstractions), Laurent Théry and Benjamin Grégoire (big numbers), Arnaud Spiwack and Pierre Letouzey (word-based arithmetic), further extensions by Pierre Letouzey; integration of Arith and ZArith to Numbers by Pierre Letouzey
+\item Classes: Matthieu Sozeau
+\item QArith: Pierre Letouzey, with contributions from Russell O'Connor
+\item Setoid: Matthieu Sozeau (first version by Clément Renard, second version by Claudio Sacerdoti Coen)
+\item Sets: Gilles Kahn and Gérard Huet
+\item Sorting: Gérard Huet with revisions by Hugo Herbelin
+\item Strings: Laurent Théry
+\item Program: Matthieu Sozeau
+\item Unicode: Claude Marché
+\end{itemize}
+
+\section{Commands}
+
+\begin{itemize}
+\item Batch compiler (\texttt{coqc}):  Chet Murthy (?)
+\item Compilation dependency calculator (\texttt{coqdep}):
+  Jean-Christophe Filliâtre
+\item Statistic tool (\texttt{coqwc}): Jean-Christophe Filliâtre
+\item Simple html presentation tool (\texttt{gallina}) (deprecated): Jean-Christophe Filliâtre
+\item Auto-maker (\texttt{coq\_makefile}): Jean-Christophe Filliâtre,
+  with contributions from Judicaël Courant, updated by Pierre Boutillier
+\item LaTeX presentation tool (\texttt{coq-tex}): Jean-Christophe Filliâtre
+\item Multi-purpose presentation tool (\texttt{coqdoc}): Jean-Christophe Filliâtre with extensions from
+  Matthieu Sozeau, Jean-Marc Notin, Hugo Herbelin and contributions from Adam Chlipala
+\item Interactive toplevel (\texttt{coqtop}): Jean-Christophe Filliâtre (?)
+\item Custom toplevel builder (\texttt{coqmktop}): Jean-Christophe Filliâtre (?)
+\end{itemize}
+
+\section{Graphical interfaces}
+
+\begin{itemize}
+\item Support for {\em Proof General}: Pierre Courtieu with contributions from Arnaud Spiwack
+\item {\em CoqIDE}: Benjamin Monate with contributions from
+  Jean-Christophe Filliâtre, Claude Marché, Pierre Letouzey, Julien
+  Narboux, Hugo Herbelin, Pierre Corbineau, Pierre Boutillier,
+  Pierre-Marie Pédrot; processus-based communication protocol by
+  Vincent Gross with contributions from Pierre Letouzey, Pierre
+  Boutillier, Pierre-Marie Pédrot; backtracking revised by Pierre
+  Letouzey; uses the Cameleon library by Maxence Guesdon;
+\end{itemize}
+
+\section{Architecture}
+
+\begin{itemize}
+\item Functional-kernel-based architecture: Jean-Christophe Filliâtre
+\item Extensible objects and summaries: Chet Murthy
+\item Hash-consing: Bruno Barras
+\item Error locations: Jean-Christophe Filliâtre, Bruno Barras, Hugo Herbelin, with contributions from Arnaud Spiwack
+\item Existential variables engine: Chet Murthy with revisions by
+  Bruno Barras and Arnaud Spiwack and extensions by Clément Renard and
+  Hugo Herbelin
+\end{itemize}
+
+\section{Development tools}
+
+\begin{itemize}
+\item Makefile's: Chet Murthy, Jean-Christophe Filliâtre, Judicaël
+  Courant, Lionel Mamane, Pierre Corbineau, Pierre Letouzey with
+  contributions from Stéphane Glondu, Hugo Herbelin, ...
+\item Debugging: Jean-Christophe Filliâtre with contributions from Jacek Chrz\k{a}szcz, Hugo Herbelin, Bruno Barras, ...
+\item ML quotations: David Delahaye and Daniel de Rauglaudre
+\item ML tactic and vernacular extensions: Hugo Herbelin (first version by Chet Murthy)
+\item Test suite: collective content, initiated by Jean-Christophe Filliâtre with further extensions by Hugo Herbelin, Jean-Marc Notin
+\end{itemize}
+
+\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 Team coordination: Gérard Huet, Christine Paulin, Hugo Herbelin,
+  with various other contributions
+\item Packaging tools: Henri Laulhere, David Delahaye, Julien Narboux,
+  Pierre Letouzey, Enrico Tassi (Windows); Damien Doligez, Hugo
+  Herbelin, Pierre Boutillier (MacOS); Jean-Christophe Filliâtre,
+  Judicaël Courant, Hugo Herbelin, Stéphane Glondu (Linux)
+\end{itemize}
+
+\section{Documentation}
+
+\begin{itemize}
+
+\item Reference Manual: collective, layout by Patrick Loiseleur,
+  Claude Marché (former User's Guide in 1991 by Gilles Dowek, Amy
+  Felty, Hugo Herbelin, Gérard Huet, Christine Paulin, Benjamin
+  Werner; initial documentation in 1989 by Thierry Coquand, Gilles
+  Dowek, Gérard Huet, Christine Paulin),
+\item Basic tutorial: Gérard Huet, Gilles Kahn, Christine Paulin
+\item Tutorial on recursive types: Eduardo Gimenez with updates by Pierre Castéran
+\item FAQ: Hugo Herbelin, Julien Narboux, Florent Kirchner
+\end{itemize}
+
+\section{Features discontinued by lack of support}
+
+\begin{itemize}
+\item Searching modulo isomorphism: David Delahaye
+\item Explanation of proofs in pseudo-natural language: Yann Coscoy
+\item Export of context to external communication tools (\texttt{dp}):
+  Nicolas Ayache and Jean-Christophe Filliâtre, with contributions by
+  Claude Marché
+\item Support for {\em PCoq}: Yves Bertot with contributions by
+  Laurence Rideau and Loïc Pottier; additional support for {\em TmEgg}
+  by Lionel Mamane
+\item Export of terms and environments to XML format: Claudio
+  Sacerdoti Coen, with extensions from Cezary Kaliszyk
+\end{itemize}
+
+For probable oversights or accidental errors, please report to Hugo~\verb=.=~Herbelin~\verb=@=~inria~\verb=.=~fr
+
+\end{document}
-- 
cgit v1.2.3