Whodidwhat-8.5: a global pass

Updating my own work and others when I could think of them.

1 files changed, 29 insertions, 22 deletions

diff --git a/doc/whodidwhat/whodidwhat-8.5update.tex b/doc/whodidwhat/whodidwhat-8.5update.tex
index c187cdb43..ce099dc36 100644
--- a/doc/whodidwhat/whodidwhat-8.5update.tex
+++ b/doc/whodidwhat/whodidwhat-8.5update.tex
@@ -73,13 +73,17 @@
 \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
+  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: Amokrane Saïbi with extensions by Arnaud Spiwack and
-  Matthieu Sozeau
+\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}...):
@@ -97,6 +101,7 @@
 \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
@@ -108,28 +113,30 @@
 \subsection{Predefined tactics}
 
 \begin{itemize}
-\item Basic tactics (\texttt{intro}, \texttt{apply},
+\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}), with contributions from Hugo Herbelin, Enrico Tassi, ...
+  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
+  {\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 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 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 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 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
@@ -180,11 +187,6 @@
 \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}
@@ -229,7 +231,7 @@
 \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 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
@@ -261,9 +263,6 @@
 \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
@@ -332,6 +331,14 @@
 \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