some credits for STM

1 files changed, 22 insertions, 2 deletions

diff --git a/doc/refman/RefMan-pre.tex b/doc/refman/RefMan-pre.tex
index b860e43db..8c169ee1e 100644
--- a/doc/refman/RefMan-pre.tex
+++ b/doc/refman/RefMan-pre.tex
@@ -938,7 +938,7 @@ Hugo Herbelin\\
 projects:
 \begin{itemize}
 \item A new asynchronous evaluation and compilation mode by Enrico
-  Tassi.
+  Tassi with help from Bruno Barras and Carst Tankink.
 \item The full integration of the new proof engine by Arnaud Spiwack
   helped by Pierre-Marie Pédrot,
 \item The addition of conversion and reduction based on native compilation
@@ -955,7 +955,27 @@ the user level Ltac language deep tactic backtracking and multi-goal
 handling. This allows 
 ...
 
-STM: Enrico
+The way Coq processes a document in batch and interactive mode has
+been redesigned by Enrico Tassi with help from Bruno Barras.  Opaque
+proofs, the text between Proof and Qed, can be processed
+asynchronously, decoupling the checking of definitions and statements
+from the checking of proofs.  In interactively this improves the
+reactiveness of the system, since proofs can be processed in the
+background.  Similarly the compilation of a file can be split into two
+phases:  the first one checking only definitions and statements and
+the second one checking proofs.  A file resulting from the first
+phase, .vio extension, can be already Required.  All .vio files can be
+turned into complete .vo files in parallel.  The same infrastructure
+also allows terminating tactics to be run in parallel on a set of
+goals via the par: goal selector.
+CoqIDE was patched to cope with asynchronous checking of the document.
+Its source code was also made separate from the one of Coq making it no
+more a special user interface and allowing its release cycle to be
+decoupled with the one of Coq.
+Carst Tankink developed a Coq back end for PIDE enabled user interfaces,
+like PIDE/jEdit (with help from Makarius Wenzel) or PIDE/Coqoon (with
+help from Alexander Faithfull and Jesper Bengtson).
+The development of such features was funded by the Paral-ITP ANR project.
 
 The universe polymorphism extension is based on a change of the kernel
 architecture to handle constraint checking only, leaving the generation