From b00500d44818b6d182bd4e8b233bc963bfbf5505 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 7 Jul 2006 15:37:23 +0000
Subject: 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
---
 doc/refman/RefMan-pre.tex | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

(limited to 'doc/refman/RefMan-pre.tex')

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}
 
-- 
cgit v1.2.3