diff options
| -rwxr-xr-x | doc/RefMan-pre.tex | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/doc/RefMan-pre.tex b/doc/RefMan-pre.tex index 62414b4636..73f6eb5b70 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$ |