MAJ

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9090 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 17 insertions, 3 deletions

diff --git a/doc/refman/RefMan-pre.tex b/doc/refman/RefMan-pre.tex
index 27a5a6c88b..6aaca96683 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\\
@@ -564,9 +567,20 @@ Pierre Corbineau extended his tactic for solving first-order
 statements. He wrote a reflection-based intuitionistic tautology
 solver.
 
+Pierre Courtieu and Julien Forest 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.
+
+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