*** empty log message ***

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

1 files changed, 6 insertions, 6 deletions

diff --git a/doc/RefMan-pre.tex b/doc/RefMan-pre.tex
index 62414b463..73f6eb5b7 100755
--- a/doc/RefMan-pre.tex
+++ b/doc/RefMan-pre.tex
@@ -2,7 +2,7 @@
 \chapter*{Credits}
 %\addcontentsline{toc}{section}{Credits}
 
-{\Coq} is a proof assistant for higher-order logic, allowing the
+\Coq{}~ is a proof assistant for higher-order logic, allowing the
 development of computer programs consistent with their formal
 specification.  It is the result of about ten years of research of the
 Coq project.  We shall briefly survey here three main aspects: the
@@ -408,12 +408,12 @@ Hugo Herbelin \& Christine Paulin
 First, the underlying logic is slightly different. The so-called {\em
 impredicativity} of the sort {\tt Set} has been dropped. The main
 reason is that it is inconsistent with the principle of description
-which is quite a useful principle for formalizing classical
+which is quite a useful principle for formalizing %classical
 mathematics within classical logic. Moreover, even in an constructive
 setting, the impredicativity of {\tt Set} does not add so much in
 practice and is even subject of criticism from a large part of the
 intuitionistic mathematician community. Nevertheless, the
-impredicativy of {\tt Set} remains optional for users interested in
+impredicativity of {\tt Set} remains optional for users interested in
 investigating mathematical developments which rely on it.
 
 Secondly, the concrete syntax of terms has been completely
@@ -491,13 +491,13 @@ types. He is also the maintainer of the non-domain specific automation
 tactics.
 
 Benjamin Monate is the developer of the \CoqIde{} graphical
-interface.
+interface with contributions by Claude Marché.
 
 Pierre Letouzey and Jacek Chrz\k{a}szcz respectively maintained the
 extraction tool and module system of {\Coq}.
 
 Jean-Christophe Filliātre, Pierre Letouzey, Hugo Herbelin and 
-contributors from Sophia-Antipolis and Nijmegen contributed to the
+contributors from Sophia-Antipolis and Nijmegen participated to the
 extension of the library.
 
 Hugo Herbelin and Christine Paulin coordinated the developement which
@@ -511,7 +511,7 @@ Hugo Herbelin \& Christine Paulin
 
 \newpage
 
-Integration of ZArith lemmas from Sophia and Nijmegen.
+% Integration of ZArith lemmas from Sophia and Nijmegen.
 
 
 % $Id$