From 1881be14416e3eb719cce90c6ac5d1f17ff53cd8 Mon Sep 17 00:00:00 2001 From: Yuval Langer Date: Thu, 7 Jul 2016 19:14:53 +0300 Subject: Fix inforef references to the emacs manual. (#88) --- doc/ProofGeneral.texi | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) (limited to 'doc') diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi index 80c4660b..05fb1b50 100644 --- a/doc/ProofGeneral.texi +++ b/doc/ProofGeneral.texi @@ -711,7 +711,7 @@ of a common interface mechanism. To get more from Proof General and adapt it to your liking, it helps to know a little bit about how Emacs lisp packages can be customized via the Customization mechanism. It's really easy to use. For details, -@pxref{How to customize}. @inforef{Customization, ,(emacs)}, +@pxref{How to customize}. @inforef{Customization, ,emacs}, for documentation in Emacs. To get the absolute most from Proof General, to improve it or to adapt @@ -1548,7 +1548,7 @@ As experienced Emacs users will know, a @i{prefix argument} is a numeric argument supplied by some key sequence typed before a command key sequence. You can supply a specific number by typing @key{Meta} with the digits, or a ``universal'' prefix of @kbd{C-u}. See -@inforef{Arguments, ,(emacs)} for more details. Several Proof General +@inforef{Arguments, ,emacs} for more details. Several Proof General commands, like @code{proof-retract-until-point-interactive}, may accept a @i{prefix argument} to adjust their behaviour somehow. @@ -2864,7 +2864,7 @@ This is an inherent problem with outline because it works by modifying the buffer. If you want to use outline with processed scripts, you can turn off the @code{Strict Read Only} option. -See @inforef{Outline Mode, ,(emacs)} for more information about outline mode. +See @inforef{Outline Mode, ,emacs} for more information about outline mode. @node Support for completion @section Support for completion @@ -2960,7 +2960,7 @@ General doesn't do this automatically. Apart from completion, there are several other operations on tags. One common one is replacing identifiers across all files using @code{tags-query-replace}. For more information on how to use tags, -@inforef{Tags, ,(emacs)}. +@inforef{Tags, ,emacs}. To use tags for completion at the same time as the completion mechanism mentioned already, you can use the command @kbd{M-x add-completions-from-tags-table}. @@ -3316,7 +3316,7 @@ Proof General has been fully loaded. Proof General is fully loaded when you visit a script file for the first time, or if you type @kbd{M-x load-library RET proof RET}. -For more help with customize, see @inforef{Customization, ,(emacs)}. +For more help with customize, see @inforef{Customization, ,emacs}. @@ -4104,7 +4104,7 @@ arbitrary code in this file @inforef{Directory Variables, ,emacs}. @section Using abbreviations A very useful package of Emacs supports automatic expansions of -abbreviations as you type, @inforef{Abbrevs, ,(emacs)}. +abbreviations as you type, @inforef{Abbrevs, ,emacs}. For example, the proof assistant Coq has many command strings that are long, such as ``reflexivity,'' ``Inductive,'' ``Definition'' and -- cgit v1.2.3