From 228c9739a6e94f52a1fd4d6439ee34af1f7a987a Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 24 Dec 2003 08:54:24 +0000
Subject: Aspect mathematique de Coq

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

diff --git a/doc/RefMan-int.tex b/doc/RefMan-int.tex
index 649cfc3a99..1595dccf57 100755
--- a/doc/RefMan-int.tex
+++ b/doc/RefMan-int.tex
@@ -8,7 +8,11 @@ A new book~\cite{CoqArt} on practical uses of the \Coq{} system will
 be published in 2004 and is a good support for both the beginner and
 the advanced user.
 
-The system \Coq\ is designed to write formal specifications,
+%The system \Coq\ is designed to develop mathematical proofs. It can be
+%used by mathematicians to develop mathematical theories and by
+%computer scientists to write formal specifications,
+The system \Coq\ is designed to develop mathematical proofs, and
+especially to write formal specifications,
 programs and to verify that programs are correct with respect to their
 specification. It provides a specification language named \gallina. Terms of
 \gallina\ can represent programs as well as properties of these
-- 
cgit v1.2.3