diff options
author | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-08-05 09:41:22 +0200 |
---|---|---|
committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-08-05 19:52:20 +0200 |
commit | 69aff8116b4878671daf73cc7ccf713aac0c0e6d (patch) | |
tree | fdf645c8ac17cbb90ea0e24cac7c2d6812a3a6f5 /doc | |
parent | cd04bf55d158f96b260a591f76cff3a2d90d79e1 (diff) |
Making references to Proof General and CoqIDE uniform in Reference Manual.
Diffstat (limited to 'doc')
-rwxr-xr-x | doc/common/macros.tex | 1 | ||||
-rw-r--r-- | doc/refman/RefMan-com.tex | 2 | ||||
-rw-r--r-- | doc/refman/RefMan-decl.tex | 4 | ||||
-rw-r--r-- | doc/refman/RefMan-int.tex | 2 | ||||
-rw-r--r-- | doc/refman/RefMan-pro.tex | 4 | ||||
-rw-r--r-- | doc/refman/RefMan-uti.tex | 6 |
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!. |