Documentation Declare Implicit Tactic, Print Canonical Projections, ... + légère restructuration autour de Proof with et Hint Rewrite + maj crédits

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

1 files changed, 6 insertions, 6 deletions

diff --git a/doc/refman/RefMan-pre.tex b/doc/refman/RefMan-pre.tex
index add22103c8..27a5a6c88b 100644
--- a/doc/refman/RefMan-pre.tex
+++ b/doc/refman/RefMan-pre.tex
@@ -556,19 +556,19 @@ unresolved implicit has been implemented by Hugo Herbelin.
 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. Pierre Letouzey's contribution on rational numbers
-has been integrated too.
+library about finite sets ``à la Objective Caml''. With Jean-Marc
+Notin, he extended the library on lists. Pierre Letouzey's
+contribution on rational numbers has been integrated and extended..
 
 Pierre Corbineau extended his tactic for solving first-order
 statements. He wrote a reflection-based intuitionistic tautology
 solver.
 
-Jean-Marc Notin took care of {\textsf{coqdoc}} and of the general
-maintenance of the system.
+Jean-Marc Notin significantly contributed to the general maintenance
+of the system. He also took care of {\textsf{coqdoc}}.
 
 \begin{flushright}
-Palaiseau, Apr. 2006\\
+Palaiseau, July 2006\\
 Hugo Herbelin
 \end{flushright}