From 79490d29774277801ccd4b7fa68dd9770bab8a6f Mon Sep 17 00:00:00 2001
From: coq
Date: Mon, 5 Jan 2004 08:30:35 +0000
Subject: correction bugs commit precedent et mise en forme html

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

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

diff --git a/doc/RefMan-pre.tex b/doc/RefMan-pre.tex
index 3603c95b2b..11cc8ce5cd 100755
--- a/doc/RefMan-pre.tex
+++ b/doc/RefMan-pre.tex
@@ -450,11 +450,11 @@ integer numbers. Finally, the names of the standard properties of
 numbers now follow a standard pattern and the symbolic
 notations for the standard definitions as well.
 
-The fourth point is the release of \CoqIde{}, a new graphical
+The fourth point is the release of \CoqIDE{}, a new graphical
 gtk2-based interface fully integrated to {\Coq}. Close in style from
 the Proof General Emacs interface, it is faster and its integration
 with {\Coq} makes interactive developments more friendly. All
-mathematical Unicode symbols are usable within \CoqIde{}.
+mathematical Unicode symbols are usable within \CoqIDE{}.
 
 Finally, the module system of {\Coq} completes the picture of {\Coq}
 version 8.0. Though released with an experimental status in the previous
@@ -483,7 +483,7 @@ tactic for solving first-order statements in presence of inductive
 types. He is also the maintainer of the non-domain specific automation
 tactics.
 
-Benjamin Monate is the developer of the \CoqIde{} graphical
+Benjamin Monate is the developer of the \CoqIDE{} graphical
 interface with contributions by Jean-Christophe Filliātre, Pierre
 Letouzey and Claude Marché.
 
-- 
cgit v1.2.3