Nouvelle MAJ

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

1 files changed, 8 insertions, 5 deletions

diff --git a/doc/refman/RefMan-pre.tex b/doc/refman/RefMan-pre.tex
index 52fe08fca7..6ef799afce 100644
--- a/doc/refman/RefMan-pre.tex
+++ b/doc/refman/RefMan-pre.tex
@@ -536,8 +536,8 @@ Benjamin Grégoire, Assia Mahboubi and Bruno Barras developed a new
 more efficient and more general simplification algorithm on rings and
 semi-rings.
 
-Hugo Herbelin, Pierre Letouzey and Claudio Sacerdoti Coen added new
-tactic features.
+Hugo Herbelin, Pierre Letouzey, Julien Forest, Julien Narboux and
+Claudio Sacerdoti Coen added new tactic features.
 
 Hugo Herbelin implemented matching on disjunctive patterns.
 
@@ -547,7 +547,8 @@ connections with the provers {\sc cvcl}, {\sc Simplify} and {\sc
 zenon}. Hugo Herbelin implemented an experimental protocol for calling
 external tools from the tactic language.
 
-%Matthieu Sozeau developed an experimental language to reason over subtypes.
+Matthieu Sozeau developed \textsc{Russell}, an experimental language
+to specify the behavior of programs with subtypes.
 
 A mechanism to automatically use some specific tactic to solve
 unresolved implicit has been implemented by Hugo Herbelin.
@@ -556,13 +557,15 @@ Laurent Théry's contribution on strings and Pierre Letouzey and
 Jean-Christophe Filliâtre's contribution on finite maps have been
 integrated to the {\Coq} standard library. Pierre Letouzey developed a
 library about finite sets ``à la Objective Caml'' and extended the
-lists library.
+lists library. Pierre Letouzey's contribution on rational numbers
+has been integrated too.
 
 Pierre Corbineau extended his tactic for solving first-order
 statements. He wrote a reflexion-based intuitionistic tautology
 solver.
 
-Jean-Marc Notin took care of the general maintenance of the system.
+Jean-Marc Notin took care of {\textsf{coqdoc}} and of the general
+maintenance of the system.
 
 \begin{flushright}
 Palaiseau, Apr. 2006\\