texinfo manuals: fix obsolete @Inforef

In most cases, this is a simple replacement, using @pxref in most
cases.

doc/PG-adapting.texi

@@ -270,7 +270,7 @@ prototype is about 25 simple settings.
 For more advanced features you may need (or want) to write some Emacs
 Lisp.  If you're adding new functionality please consider making it
 generic for different proof assistants, if appropriate.  When writing
-your modes, please follow the Emacs Lisp conventions, @inforef{Tips, ,Elisp}.
+your modes, please follow the Emacs Lisp conventions, @pxref{Tips,,,Elisp}.
 
 The configuration variables are declared in the file
 @file{generic/proof-config.el}.  The details in the central part of this
@@ -667,7 +667,7 @@ Note that for the generic functions to work properly, it is
 @strong{essential} that you set the syntax table for your mode properly,
 so that comments and strings are recognized.  See the Emacs
 documentation to discover how to do this (particularly for the function
-@code{modify-syntax-entry}, (@inforef{Syntax Tables, ,Elisp}).
+@code{modify-syntax-entry}, (@pxref{Syntax Tables,,,Elisp}).
 
 @xref{Proof script mode}, for more details of the parsing
 functions.
@@ -730,7 +730,7 @@ or @samp{@code{proof-script-parse-function}}.
 The next four settings configure the comment syntax.  Notice that to get
 reliable behaviour of the parsing functions, you may need to modify the
 syntax table for your prover's mode.  
-Read the Elisp manual (@inforef{Syntax Tables, ,Elisp}) for details about that.
+Read the Elisp manual (@pxref{Syntax Tables,,,Elisp}) for details about that.
 
 @c TEXI DOCSTRING MAGIC: proof-script-comment-start
 @defvar proof-script-comment-start 
@@ -1148,9 +1148,9 @@ consistency. Portions that can be potentially omitted are called
 @emph{opaque proofs} in Proof General, because usually only
 opaque proofs (in the sense of Coq) can be omitted without
 risking to break the following code. This feature is also
-described in the Proof General manual, @inforef{Script processing
-commands, ,ProofGeneral} and @inforef{Omitting proofs for speed,
-,ProofGeneral}.
+described in the Proof General manual, @pxref{Script processing
+commands,,,ProofGeneral} and
+@pxref{Omitting proofs for speed,,,ProofGeneral}.
 
 The omit proofs feature works in a simple, straightforward way:
 After parsing the asserted region, Proof General uses regular
@@ -2519,7 +2519,8 @@ advantage of not requiring the underlying text to be changed to display
 symbols.  
 
 Usage of the Unicode Tokens package is described in the Proof General
-user manual, @inforef{Unicode support, ,ProofGeneral}.
+user manual, @pxref{Unicode symbols and special layout
+support,,,ProofGeneral}.
 
 @c FIXME TODO: add documentation here to explain config of Unicode Tokens
 

doc/ProofGeneral.texi

@@ -743,7 +743,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}.  @xref{Customization,,,emacs},
 for documentation in Emacs.
 
 To get the absolute most from Proof General, to improve it or to adapt
@@ -1622,7 +1622,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
+@ref{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.
 
@@ -2927,7 +2927,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 @ref{Outline Mode,,,emacs} for more information about outline mode.
 
 @node Support for completion
 @section Support for completion
@@ -3023,7 +3023,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}.
+@pxref{xref,,,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}.
@@ -3379,7 +3379,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 @ref{Customization,,,emacs}.
 
 
 
@@ -4100,7 +4100,7 @@ and a short-cut for enabling three window mode,
 @cindex file variables
 
 A very convenient way to customize file-specific variables is to use 
-File Variables (@inforef{File Variables, ,emacs}). This feature of
+File Variables (@pxref{File Variables,,,emacs}). This feature of
 Emacs permits to specify values for certain Emacs variables
 when a file is loaded. File variables and their values 
 are written as a list at the end of
@@ -4144,13 +4144,13 @@ And then the right call to make will be done if you use the @kbd{M-x
 compile} command, and the correct @code{coqtop} will be called by
 ProofGeneral. Note that the lines are commented in order to be ignored
 by the proof assistant. It is possible to use this mechanism for all
-variables, @inforef{File Variables, ,emacs}.
+variables, @pxref{File Variables,,,emacs}.
 
 @emph{NOTE:} @code{coq-prog-name} should contain only the @code{coqtop}
 executable, @emph{not the options}.
 
 One can also specify file variables on a per directory basis,
-@inforef{Directory Variables, ,emacs}. You can achieve almost the same
+@pxref{Directory Variables,,,emacs}. You can achieve almost the same
 as above for all the files of a directory by storing
 
 @lisp
@@ -4161,7 +4161,7 @@ as above for all the files of a directory by storing
 into the file @code{.dir-locals.el} in one of the parent directories.
 The value in this file must be an alist that maps mode names to alists,
 where these latter alists map variables to values. You can aso put
-arbitrary code in this file @inforef{Directory Variables, ,emacs}.
+arbitrary code in this file @pxref{Directory Variables,,,emacs}.
 
 @emph{Note:} if you add such content to the @code{.dir-locals.el} file
 you should restart Emacs or revert your buffer.
@@ -4170,7 +4170,7 @@ you should restart Emacs or revert your buffer.
 @section Using abbreviations
 
 A very useful package of Emacs supports automatic expansions of
-abbreviations as you type, @inforef{Abbrevs, ,emacs}.
+abbreviations as you type, @pxref{Abbrevs,,,emacs}.
 
 For example, the proof assistant Coq has many command strings that are
 long, such as ``reflexivity,'' ``Inductive,'' ``Definition'' and
@@ -4314,10 +4314,12 @@ with the option @code{coq-load-path}, but this is not compatible
 with @code{CoqIde} or @code{coq_makefile}.
 
 @emph{NOTE:} the Coq project file cannot define which version of
-@code{coqtop} is launched. You need either to launch emacs with the
-right executable in the path or use @inforef{File Variables, ,emacs} or
-@inforef{Directory Variables, ,emacs}. See @ref{Using file variables}
-below.
+@code{coqtop} is launched. @xref{Opam-switch-mode support} for how to
+switch between different Coq versions. Alternatively, for a fixed
+version, you need either to launch emacs with the right executable in
+the path or use file variables (@pxref{Using file variables} below or
+@pxref{File Variables,,,emacs}) or directory variables,
+@pxref{Directory Variables,,,emacs}.
 
 @menu
 * Changing the name of the coq project file::
@@ -4338,7 +4340,7 @@ If you only want to change the name of the Coq project file for
 one project you can set the option as local file variable,
 @ref{Using file variables}. This can be done either directly in
 every file or once for all files of a directory tree with a
-@code{.dir-locals.el} file, @inforef{Directory Variables, ,emacs}.
+@code{.dir-locals.el} file, @pxref{Directory Variables,,,emacs}.
 The file @code{.dir-locals.el} should then contain
 
 @lisp
@@ -4543,7 +4545,7 @@ Output from the compilation is only shown in case
 of errors. It then appears in the buffer
 @code{*coq-compile-response*}.
 One can use @code{C-x `} (bound to @code{next-error},
-@inforef{Compilation Mode,,emacs}) to jump to error locations.
+@pxref{Compilation Mode,,,emacs}) to jump to error locations.
 Sometimes the compilation commands do not produce error messages
 with location information, then @code{C-x `} does only work in a
 limited way.