1 files changed, 24 insertions, 4 deletions
diff --git a/doc/refman/RefMan-pre.tex b/doc/refman/RefMan-pre.tex
index 43216ed0..8b6e29b5 100644
--- a/doc/refman/RefMan-pre.tex
+++ b/doc/refman/RefMan-pre.tex
@@ -379,6 +379,9 @@ Mathematics (HELM cf \url{http://www.cs.unibo.it/helm}).
 A library for efficient representation of finite maps using binary trees
 contributed by Jean Goubault was integrated in the basic theories.
 
+Pierre Courtieu developed a command and a tactic to reason on the
+inductive structure of recursively defined functions.
+
 Jacek Chrz\k{a}szcz designed and implemented the module system of
 {\Coq} whose foundations are in Judicaël Courant's PhD thesis.
 
@@ -388,12 +391,12 @@ The development was coordinated by C. Paulin.
 
 Many discussions within the Démons team and the LogiCal project
 influenced significantly the design of {\Coq} especially with 
-%J. Chrz\k{a}szcz, 
-J. Courant, P. Courtieu, J. Duprat, J. Goubault, A. Miquel,
+%J. Chrz\k{a}szcz, P. Courtieu, 
+J. Courant, J. Duprat, J. Goubault, A. Miquel,
 C. Marché, B. Monate and B. Werner.
 
 Intensive users suggested improvements of the system : 
-Y. Bertot, L. Pottier, L. Théry , P. Zimmerman from INRIA, 
+Y. Bertot, L. Pottier, L. Théry, P. Zimmerman from INRIA, 
 C. Alvarado, P. Crégut, J.-F. Monin from France Telecom R \& D.
 \begin{flushright}
 Orsay, May. 2002\\
@@ -536,6 +539,9 @@ Benjamin Grégoire, Assia Mahboubi and Bruno Barras developed a new
 more efficient and more general simplification algorithm on rings and
 semi-rings.
 
+Laurent Théry and Bruno Barras developed a new significantly more efficient
+simplification algorithm on fields.
+
 Hugo Herbelin, Pierre Letouzey, Julien Forest, Julien Narboux and
 Claudio Sacerdoti Coen added new tactic features.
 
@@ -564,9 +570,23 @@ Pierre Corbineau extended his tactic for solving first-order
 statements. He wrote a reflection-based intuitionistic tautology
 solver.
 
+Pierre Courtieu, Julien Forest and Yves Bertot added extra support to
+reason on the inductive structure of recursively defined functions.
+
 Jean-Marc Notin significantly contributed to the general maintenance
 of the system. He also took care of {\textsf{coqdoc}}.
 
+Pierre Castéran contributed to the documentation of (co-)inductive
+types and suggested improvements to the libraries.
+
+Pierre Corbineau implemented a declarative mathematical proof
+language, usable in combination with the tactic-based style of proof.
+
+Finally, many users suggested improvements of the system through the
+Coq-Club mailing list and bug-tracker systems, especially user groups
+from INRIA Rocquencourt, Radbout University, University of
+Pennsylvania and Yale University.
+
 \begin{flushright}
 Palaiseau, July 2006\\
 Hugo Herbelin
@@ -577,7 +597,7 @@ Hugo Herbelin
 % Integration of ZArith lemmas from Sophia and Nijmegen.
 
 
-% $Id: RefMan-pre.tex 9030 2006-07-07 15:37:23Z herbelin $ 
+% $Id: RefMan-pre.tex 9283 2006-10-26 08:13:51Z herbelin $ 
 
 %%% Local Variables: 
 %%% mode: latex