6 files changed, 10 insertions, 9 deletions
diff --git a/doc/common/macros.tex b/doc/common/macros.tex
index 2704a28af..c5538aaab 100755
--- a/doc/common/macros.tex
+++ b/doc/common/macros.tex
@@ -96,6 +96,7 @@
 \newcommand{\ocaml}{\textsc{Objective Caml}}
 \newcommand{\camlpppp}{\textsc{Camlp4}}
 \newcommand{\emacs}{\textsc{GNU Emacs}}
+\newcommand{\ProofGeneral}{\textsc{Proof General}}
 \newcommand{\CIC}{\pCIC}
 \newcommand{\pCIC}{p\textsc{Cic}}
 \newcommand{\iCIC}{\textsc{Cic}}
diff --git a/doc/refman/RefMan-com.tex b/doc/refman/RefMan-com.tex
index 87ec076fa..b010e6e18 100644
--- a/doc/refman/RefMan-com.tex
+++ b/doc/refman/RefMan-com.tex
@@ -179,7 +179,7 @@ Section~\ref{LongNames}).
 
 \item[{\tt -with-geoproof} (yes|no)]\ 
 
-  Activate or not special functions for Geoproof within Coqide (default is yes).
+  Activate or not special functions for Geoproof within {\CoqIDE} (default is yes).
 
 \item[{\tt -beautify}]\ 
 
diff --git a/doc/refman/RefMan-decl.tex b/doc/refman/RefMan-decl.tex
index ba8a5ac63..9015b8ec3 100644
--- a/doc/refman/RefMan-decl.tex
+++ b/doc/refman/RefMan-decl.tex
@@ -65,8 +65,8 @@ The \DPL{} is available for all Coq interfaces that use
 text-based interaction, including:
 \begin{itemize}
 \item the command-{}line toplevel {\texttt{coqtop}}
-\item the native GUI {\texttt{coqide}}
-\item the Proof-{}General emacs mode
+\item the native GUI {\CoqIDE}
+\item the {\ProofGeneral} Emacs mode
 \item Cezary Kaliszyk'{}s Web interface
 \item L.E. Mamane'{}s tmEgg TeXmacs plugin
 \end{itemize}
diff --git a/doc/refman/RefMan-int.tex b/doc/refman/RefMan-int.tex
index 6d2c37f75..fbeccb664 100644
--- a/doc/refman/RefMan-int.tex
+++ b/doc/refman/RefMan-int.tex
@@ -51,7 +51,7 @@ These two modes are documented in Chapter~\ref{Addoc-coqc}.
 
 Other modes of interaction with \Coq{} are possible: through an emacs
 shell window, an emacs generic user-interface for proof assistant
-(ProofGeneral~\cite{ProofGeneral}) or through a customized interface
+({\ProofGeneral}~\cite{ProofGeneral}) or through a customized interface
 (PCoq~\cite{Pcoq}).  These facilities are not documented here.  There
 is also a \Coq{} Integrated Development Environment described in
 Chapter~\ref{Addoc-coqide}.
diff --git a/doc/refman/RefMan-pro.tex b/doc/refman/RefMan-pro.tex
index bf02991e0..bfd045d47 100644
--- a/doc/refman/RefMan-pro.tex
+++ b/doc/refman/RefMan-pro.tex
@@ -287,7 +287,7 @@ Proof.
     assumption.
 \end{coq_example*}
 
-Remark: In ProofGeneral (emacs interface to coq), you must use bullets
+Remark: In {\ProofGeneral} (Emacs interface to {\Coq}), you must use bullets
 with this priority ordering to have a correct indentation: {\tt -},
 {\tt +}, {\tt *}. That is {\tt -} must be the outer bullet and {\tt *}
 the inner one, like in the example above.
@@ -370,7 +370,7 @@ If the current goal begins by at least one product, this command
 prints the name of the first product, as it would be generated by 
 an anonymous {\tt Intro}. The aim of this command is to ease the
 writing of more robust scripts. For example, with an appropriate 
-Proof General macro, it is possible to transform any anonymous {\tt
+{\ProofGeneral} macro, it is possible to transform any anonymous {\tt
   Intro} into a qualified one such as {\tt Intro y13}.
 In the case of a non-product goal, it prints nothing. 
 
diff --git a/doc/refman/RefMan-uti.tex b/doc/refman/RefMan-uti.tex
index f51784456..a39ece69a 100644
--- a/doc/refman/RefMan-uti.tex
+++ b/doc/refman/RefMan-uti.tex
@@ -186,9 +186,9 @@ An inferior mode to run \Coq\ under Emacs, by Marco Maggesi, is also
 included in the distribution, in file \texttt{coq-inferior.el}.
 Instructions to use it are contained in this file.
 
-\subsection[Proof General]{Proof General\index{Proof General}}
+\subsection[{\ProofGeneral}]{{\ProofGeneral}\index{\ProofGeneral}}
 
-Proof General is a generic interface for proof assistants based on
+{\ProofGeneral} is a generic interface for proof assistants based on
 Emacs. The main idea is that the \Coq\ commands you are
 editing are sent to a \Coq\ toplevel running behind Emacs and the
 answers of the system automatically inserted into other Emacs buffers. 
@@ -196,7 +196,7 @@ Thus you don't need to copy-paste the \Coq\ material from your files
 to the \Coq\ toplevel or conversely from the \Coq\ toplevel to some
 files. 
 
-Proof General is developped and distributed independently of the
+{\ProofGeneral} is developed and distributed independently of the
 system \Coq. It is freely available at \verb!proofgeneral.inf.ed.ac.uk!.