From 31dd386cbd48502033ab5ff3503d73c9ddb6fda3 Mon Sep 17 00:00:00 2001
From: mohring
Date: Thu, 19 Apr 2001 11:12:21 +0000
Subject: Mise a jour credits V7

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8190 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 doc/RefMan-pre.tex | 8 ++++++--
 1 file changed, 6 insertions(+), 2 deletions(-)

diff --git a/doc/RefMan-pre.tex b/doc/RefMan-pre.tex
index 6969ffd565..a60d98dca3 100755
--- a/doc/RefMan-pre.tex
+++ b/doc/RefMan-pre.tex
@@ -323,7 +323,6 @@ for type-checking terms. His approach was to use functional
 data-structures in order to get more sharing, to prepare the addition
 of modules and also to get closer to a certified kernel.
 
-
 H. Herbelin introduced a new structure of terms with local
 definitions and redesigned the translation from the high-level
 language of Coq to the internal representation, in particular 
@@ -343,7 +342,12 @@ even involving universes and strong elimination.
 B. Barras improved the reduction strategy for lazy evaluation. 
 
 Y. Bertot designed  the \texttt{SearchPattern} and
-\texttt{SearchRewrite} tools. 
+\texttt{SearchRewrite} tools and the support for the pcoq interface 
+(\url{http://www-sop.inria.fr/lemme/pcoq/}).
+
+C. Sacerdotti helped by H. Herbelin designed an XML output for the Coq
+modules to be used in the Hypertextual Electronic Library of
+Mathematics (HELM cf \url{http://www.cs.unibo.it/helm}).
 
 A library for efficient representation of finite sets by binary trees
 contributed by J. Goubault was integrated in the basic theories.\\
-- 
cgit v1.2.3