update manuals with make magic

2 files changed, 143 insertions, 150 deletions

diff --git a/doc/PG-adapting.texi b/doc/PG-adapting.texi
index 8bb581dc..6f9c8142 100644
--- a/doc/PG-adapting.texi
+++ b/doc/PG-adapting.texi
@@ -348,10 +348,10 @@ Each entry is a list of the form
 The @var{name} is a string, naming the proof assistant.
 The @var{symbol} is used to form the name of the mode for the
 assistant, @samp{SYMBOL-mode}, run when files with @var{automode-regexp}
-(or with extension @var{file-extension}) are visited. If present,
+(or with extension @var{file-extension}) are visited.  If present,
 @var{ignored-extensions-list} is a list of file-name extensions to be
 ignored when doing file-name completion (@var{ignored-extensions-list}
-is added to @code{completion-ignored-extensions}).
+is added to @samp{@code{completion-ignored-extensions}}).
 
 @var{symbol} is also used to form the name of the directory and elisp
 file for the mode, which will be
@@ -361,7 +361,7 @@ file for the mode, which will be
 where @var{proof-home-directory} is the value of the
 variable @samp{@code{proof-home-directory}}.
 
-The default value is @code{((isar "Isabelle" "thy") (coq "Coq" "v" nil (".vo" ".glob")) (easycrypt "EasyCrypt" "ec" ".*\\.eca?") (pgshell "PG-Shell" "pgsh") (pgocaml "PG-OCaml" "pgml") (pghaskell "PG-Haskell" "pghci"))}.
+The default value is @code{((isar "Isabelle" "thy") (coq "Coq" "v" nil (".vo" ".glob")) (easycrypt "EasyCrypt" "ec" "\\.eca?\\'") (phox "PhoX" "phx" nil (".phi" ".pho")) (pgshell "PG-Shell" "pgsh") (pgocaml "PG-OCaml" "pgml") (pghaskell "PG-Haskell" "pghci"))}.
 @end defopt
 
 
@@ -689,7 +689,7 @@ If non-nil, electric terminator does not actually insert a terminator.
 @end defvar
 @c TEXI DOCSTRING MAGIC: proof-script-sexp-commands
 @defvar proof-script-sexp-commands 
-Non-nil if script has LISP-like syntax: commands are @code{top-level} sexps.@*
+Non-nil if script has Lisp-like syntax: commands are @code{top-level} sexps.@*
 You should set this variable in script mode configuration.
 
 To configure command recognition properly, you must set at least one
@@ -842,9 +842,9 @@ It's safe to leave this setting as nil.
 @defvar proof-goal-with-hole-result 
 How to get theorem name after @samp{@code{proof-goal-with-hole-regexp}} match.@*
 String or Int.
-If an int N use @code{match-string} to recover the value of the Nth parenthesis matched.
-If it is a string use @code{replace-match}. In this case, @code{proof-save-with-hole-regexp}
-should match the entire command
+If an int N, use @samp{@code{match-string}} to get the value of the Nth parenthesis matched.
+If a string, use @samp{@code{replace-match}}.  In this case, @samp{@code{proof-goal-with-hole-regexp}}
+should match the entire command.
 @end defvar
 
 @c TEXI DOCSTRING MAGIC: proof-save-command-regexp
@@ -1229,10 +1229,10 @@ switching to B.
 @defvar proof-no-fully-processed-buffer 
 Set to t if buffers should always retract before scripting elsewhere.@*
 Leave at nil if fully processed buffers make sense for the current
-proof assistant. If nil the user can choose to fully assert a
-buffer when starting scripting in a different buffer. If t there
+proof assistant.  If nil the user can choose to fully assert a
+buffer when starting scripting in a different buffer.  If t there
 is only the choice to fully retract the active buffer before
-starting scripting in a different buffer. This last behavior is
+starting scripting in a different buffer.  This last behavior is
 needed for Coq.
 @end defvar
 
@@ -1971,7 +1971,7 @@ This setting is used inside the function @samp{@code{proof-format-filename}}.
 The value of @samp{@code{process-connection-type}} for the proof shell.@*
 Set non-nil for ptys, nil for pipes.
 
-@var{note}: In emacs >= 24 (checked for 24 and 25.0.50.1), t is not a
+@var{note}: In Emacs >= 24 (checked for 24 and 25.0.50.1), t is not a
 good choice: input is cut after @var{4095} chars, which hangs pg.
 @end defvar
 
@@ -2547,7 +2547,7 @@ commands that add new goals to a proof.
 @defvar proof-tree-new-layer-command-regexp 
 Regexp to match proof commands that add new goals to a proof.@*
 This regexp must match the command that turns the proof assistant
-into prover mode, which adds the initial goal to the proof. It
+into prover mode, which adds the initial goal to the proof.  It
 must further match commands that add additional goals after all
 previous goals have been proved.
 @end defvar
@@ -2673,13 +2673,13 @@ Elisp code maintains the following two state variables.
 Hash table to remember sequent ID's.@*
 Needed because some proof assistants do not distinguish between
 new subgoals, which have been created by the last proof command,
-and older, currently unfocussed subgoals. If Proof General meets
+and older, currently unfocussed subgoals.  If Proof General meets
 a goal, it is treated as new subgoal if it is not in this hash yet.
 
-The hash is mostly used as a set of sequent ID's. However, for
+The hash is mostly used as a set of sequent ID's.  However, for
 undo operations it is necessary to delete all those sequents from
 the hash that have been created in a state later than the undo
-state. For this purpose this hash maps sequent ID's to the state
+state.  For this purpose this hash maps sequent ID's to the state
 number in which the sequent has been created.
 
 The hash table is initialized in @samp{@code{proof-tree-start-process}}.
@@ -2690,9 +2690,9 @@ The hash table is initialized in @samp{@code{proof-tree-start-process}}.
 @defvar proof-tree-existentials-alist 
 Alist mapping existential variables to sequent ID's.@*
 Used to remember which goals need a refresh when an existential
-variable gets instantiated. To support undo commands the old
+variable gets instantiated.  To support undo commands the old
 contents of this list must be stored in
-@samp{@code{proof-tree-existentials-alist-history}}. To ensure undo is
+@samp{@code{proof-tree-existentials-alist-history}}.  To ensure undo is
 properly working, this variable should only be changed by using
 @samp{@code{proof-tree-delete-existential-assoc}},
 @samp{@code{proof-tree-add-existential-assoc}} or
@@ -2776,10 +2776,10 @@ that starts external proof-tree display.
 @defvar proof-tree-external-display 
 Display proof trees in external prooftree windows if t.@*
 Actually, if this variable is t then the user requested an
-external proof-tree display. If there was no unfinished proof
+external proof-tree display.  If there was no unfinished proof
 when proof-tree display was requested and if no proof has been
 started since then, then there is obviously no proof-tree
-display. In this case, this variable stays t and the proof-tree
+display.  In this case, this variable stays t and the proof-tree
 display will be started for the next proof.
 
 Controlled by @samp{@code{proof-tree-external-display-toggle}}.
@@ -2805,10 +2805,10 @@ message.
 @deffn Command proof-tree-external-display-toggle 
 Toggle the external proof-tree display.@*
 When called outside a proof the external proof-tree display will
-be enabled for the next proof. When called inside a proof the
-proof display will be created for the current proof. If the
+be enabled for the next proof.  When called inside a proof the
+proof display will be created for the current proof.  If the
 external proof-tree display is currently on, then this toggle
-will switch it off. At the end of the proof the proof-tree
+will switch it off.  At the end of the proof the proof-tree
 display is switched off.
 @end deffn
 
@@ -2835,7 +2835,7 @@ the current output does not come from a command (with the
 
 Urgent actions are only needed if the external proof display is
 currently running. Therefore this function should not be called
-when @samp{@code{proof-tree-external-display}} is nil. 
+when @samp{@code{proof-tree-external-display}} is nil.
 
 This function assumes that the prover output is not suppressed.
 Therefore, @samp{@code{proof-tree-external-display}} being t is actually a
@@ -2862,7 +2862,7 @@ assistant is already busy with the next item from
 @defun proof-tree-handle-delayed-output old-proof-marker cmd flags span
 Process delayed output for prooftree.@*
 This function is the main entry point of the Proof General
-prooftree support. It examines the delayed output in order to
+prooftree support.  It examines the delayed output in order to
 take appropriate actions and maintains the internal state.
 
 The delayed output to handle is in the region
@@ -2872,7 +2872,7 @@ which contains the position of @samp{@code{proof-marker}}, before the next
 command was sent to the proof assistant.
 
 All other arguments are (former) fields of the @samp{@code{proof-action-list}}
-entry that is now finally retired. @var{cmd} is the command, @var{flags} are
+entry that is now finally retired.  @var{cmd} is the command, @var{flags} are
 the flags and @var{span} is the span.
 @end defun
 
@@ -3102,8 +3102,7 @@ before and after sending the command.
 In case @var{cmd} is (or yields) nil, do nothing.
 
 @var{invisiblecallback} will be invoked after the command has finished,
-if it is set. It should probably run the hook variables
-@samp{@code{proof-state-change-pre-hook}} and
+if it is set.  It should probably run the hook variables
 @samp{@code{proof-state-change-hook}}.
 
 @var{flags} are additional flags to put onto the @samp{@code{proof-action-list}}.
@@ -3124,13 +3123,14 @@ KEY is added onto proof assistant map.
 
 @c TEXI DOCSTRING MAGIC: proof-define-assistant-command
 @deffn Macro proof-define-assistant-command 
-Define FN (docstring DOC) to send @var{body} to prover, based on @var{cmdvar}.@*
+Define FN (docstring DOC): check if @var{cmdvar} is set, then send @var{body} to prover.@*
 @var{body} defaults to @var{cmdvar}, a variable.
 @end deffn
 
 @c TEXI DOCSTRING MAGIC: proof-define-assistant-command-witharg
 @deffn Macro proof-define-assistant-command-witharg 
-Define command FN to prompt for string @var{cmdvar} to proof assistant.@*
+Define FN (arg) with DOC: check @var{cmdvar} is set, @var{prompt} a string and eval @var{body}.@*
+The @var{body} can contain occurrences of arg.
 @var{cmdvar} is a variable holding a function or string.  Automatically has history.
 @end deffn
 
@@ -3218,10 +3218,10 @@ is located in, or to the variable of the environment variable
 
 @c TEXI DOCSTRING MAGIC: proof-home-directory
 @defvar proof-home-directory 
-Directory where Proof General is installed.  Ends with slash.@*
-Default value taken from environment variable @samp{PROOFGENERAL_HOME} if set,
-otherwise based on where the file @samp{proof-site.el} was loaded from.
-You can use customize to set this variable.
+Directory where Proof General is installed.@*
+Based on where the file @samp{proof-site.el} was loaded from.
+Falls back to consulting the environment variable @samp{PROOFGENERAL_HOME} if
+proof-site.el couldn't know where it was executed from.
 @end defvar
 
 @c They're no longer options.
@@ -3254,7 +3254,7 @@ in the @code{proof-assistants} setting.
 @c TEXI DOCSTRING MAGIC: proof-assistants
 @defopt proof-assistants 
 Choice of proof assistants to use with Proof General.@*
-A list of symbols chosen from: @code{'isar} @code{'coq} @code{'easycrypt} @code{'pgshell} @code{'pgocaml} @code{'pghaskell}.
+A list of symbols chosen from: @code{'isar} @code{'coq} @code{'easycrypt} @code{'phox} @code{'pgshell} @code{'pgocaml} @code{'pghaskell}.
 If nil, the default will be ALL available proof assistants.
 
 Each proof assistant defines its own instance of Proof General,
@@ -3319,7 +3319,7 @@ but which the user may require different values of across provers.
 The function proof-assistant-<SYM> is also defined, which can be used in the
 generic portion of Proof General to access the value for the current prover.
 
-Arguments are as for @samp{defcustom}, which see.  If a :group argument is
+Arguments @var{args} are as for @samp{defcustom}, which see.  If a :group argument is
 not supplied, the setting will be added to the internal settings for the
 current prover (named <PA>-config).
 @end deffn
@@ -3614,7 +3614,7 @@ retract or assert, or automatically take the action indicated in the
 user option @samp{@code{proof-auto-action-when-deactivating-scripting}}.
 
 If @samp{@code{proof-no-fully-processed-buffer}} is t there is only the choice
-to fully retract the active scripting buffer. In this case the
+to fully retract the active scripting buffer.  In this case the
 active scripting buffer is retracted even if it was fully processed.
 Setting @samp{@code{proof-auto-action-when-deactivating-scripting}} to @code{'process}
 is ignored in this case.
@@ -3708,8 +3708,8 @@ the locked region.  If invoked outside the locked region, undo
 the last successfully processed command.  See @samp{@code{proof-retract-target}}.
 
 After retraction has succeeded in the prover, the filter will call
-@samp{@code{proof-done-retracting}}.  If @var{undo-action} is non-nil, it will 
-then be invoked on the region in the proof script corresponding to 
+@samp{@code{proof-done-retracting}}.  If @var{undo-action} is non-nil, it will
+then be invoked on the region in the proof script corresponding to
 the proof command sequence.
 @var{displayflags} control output shown to user, see @samp{@code{proof-action-list}}.
 
@@ -3721,7 +3721,7 @@ of effects:
 for scripting again which may involve retracting
 other (dependent) files.
 
-2. We may query the user whether to save some buffers.  
+2. We may query the user whether to save some buffers.
 
 Step 2 may seem odd -- we're undoing (in) the buffer, after all
 -- but what may happen is that when scripting starts going
@@ -3740,8 +3740,8 @@ proof assistant exits, we use the functions
 @defun proof-restart-buffers buffers
 Remove all extents in @var{buffers} and maybe reset @samp{@code{proof-script-buffer}}.@*
 The high-level effect is that all members of @var{buffers} are
-completely unlocked, including all the necessary cleanup. No
-effect on a buffer which is nil or killed. If one of the buffers
+completely unlocked, including all the necessary cleanup.  No
+effect on a buffer which is nil or killed.  If one of the buffers
 is the current scripting buffer, then @samp{@code{proof-script-buffer}} will
 deactivated.
 @end defun
@@ -3817,12 +3817,12 @@ The value is a list of lists of the form
 @end lisp
 which is the queue of things to do.
 
-@var{span} is a region in the sources, where @var{commands} come from. Often,
+@var{span} is a region in the sources, where @var{commands} come from.  Often,
 additional properties are recorded as properties of @var{span}.
 
 @var{commands} is a list of strings, holding the text to be send to the
-prover. It might be the empty list if nothing needs to be sent to
-the prover, such as, for comments. Usually @var{commands}
+prover.  It might be the empty list if nothing needs to be sent to
+the prover, such as, for comments.  Usually @var{commands}
 contains just 1 string, but it might also contains more elements.
 The text should be obtained with
 @samp{(mapconcat }identity @var{commands} " ")', where the last argument
@@ -3870,14 +3870,13 @@ until the asynchronous background compilation finishes.
 Signals that some items are waiting outside of @samp{@code{proof-action-list}}.@*
 If this is t it means that some items from the queue region are
 waiting for being processed in a place different from
-@samp{@code{proof-action-list}}. In this case Proof General must behave as if
-@samp{@code{proof-action-list}} would be non-empty, when it is, in fact,
-empty.
+@samp{@code{proof-action-list}}.  In this case Proof General must behave as if
+@samp{@code{proof-action-list}} would be non-empty, when it is, in fact, empty.
 
 This is used, for instance, for parallel background compilation
 for Coq: The Require command and the following items are not put
 into @samp{@code{proof-action-list}} and are stored somewhere else until the
-background compilation finishes. Then those items are put into
+background compilation finishes.  Then those items are put into
 @samp{@code{proof-action-list}} for getting processed.
 @end defvar
 
@@ -3927,7 +3926,7 @@ Query the user and exit the proof process.
 
 This simply kills the @samp{@code{proof-shell-buffer}} relying on the hook function
 
-@samp{@code{proof-shell-kill-function}} to do the hard work. If optional
+@samp{@code{proof-shell-kill-function}} to do the hard work.  If optional
 argument @var{dont-ask} is non-nil, the proof process is terminated
 without confirmation.
 
@@ -4026,9 +4025,9 @@ single string.
 The @var{action} argument is a symbol which is typically the name of a
 callback for when each string has been processed.
 
-This calls @samp{@code{proof-shell-insert-hook}}.  The arguments @samp{action} and
-@samp{scriptspan} may be examined by the hook to determine how to modify
-the @samp{string} variable (exploiting dynamic scoping) which will be
+This calls @samp{@code{proof-shell-insert-hook}}.  The arguments @var{action} and
+@var{scriptspan} may be examined by the hook to determine how to modify
+the string variable (exploiting dynamic scoping) which will be
 the command actually sent to the shell.
 
 Note that the hook is not called for the empty (null) string
@@ -4052,9 +4051,8 @@ not need to use these directly.
 @c TEXI DOCSTRING MAGIC: proof-grab-lock
 @defun proof-grab-lock &optional queuemode
 Grab the proof shell lock, starting the proof assistant if need be.@*
-Runs @samp{@code{proof-state-change-pre-hook}} and
-@samp{@code{proof-state-change-hook}} to notify state change. If
-@var{queuemode} is supplied, set the lock to that value.
+Runs @samp{@code{proof-state-change-hook}} to notify state change.
+If @var{queuemode} is supplied, set the lock to that value.
 @end defun
 
 @c TEXI DOCSTRING MAGIC: proof-release-lock
@@ -4256,8 +4254,8 @@ Marker in proof shell buffer pointing to end of last urgent message.
 @defun proof-shell-process-urgent-message start end
 Analyse urgent message between @var{start} and @var{end} for various cases.
 
-Cases are: @strong{trace} output, included/retracted files, cleared 
-goals/response buffer, variable setting, xml-encoded @var{pgip} response, 
+Cases are: @strong{trace} output, included/retracted files, cleared
+goals/response buffer, variable setting, xml-encoded @var{pgip} response,
 theorem dependency message or interactive output indicator.
 
 If none of these apply, display the text between @var{start} and @var{end}.
@@ -4279,13 +4277,13 @@ library that is distributed with Proof General (in
 Master filter for the proof assistant shell-process.@*
 A function for @samp{@code{scomint-output-filter-functions}}.
 
-Deal with output and issue new input from the queue. This is an
-important internal function. The output must be collected from
-@samp{@code{proof-shell-buffer}} for the following reason. This function
+Deal with output and issue new input from the queue.  This is an
+important internal function.  The output must be collected from
+@samp{@code{proof-shell-buffer}} for the following reason.  This function
 might block inside @samp{@code{process-send-string}} when sending input to
-the proof assistant or to prooftree. In this case Emacs might
+the proof assistant or to prooftree.  In this case Emacs might
 call the process filter again while the previous instance is
-still running. @samp{@code{proof-shell-filter-wrapper}} detects and delays
+still running.  @samp{@code{proof-shell-filter-wrapper}} detects and delays
 such calls but does not buffer the output.
 
 Handle urgent messages first.  As many as possible are processed,
diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi
index dfa09085..aca9d21e 100644
--- a/doc/ProofGeneral.texi
+++ b/doc/ProofGeneral.texi
@@ -1728,7 +1728,7 @@ Query the user and exit the proof process.
 
 This simply kills the @samp{@code{proof-shell-buffer}} relying on the hook function
 
-@samp{@code{proof-shell-kill-function}} to do the hard work. If optional
+@samp{@code{proof-shell-kill-function}} to do the hard work.  If optional
 argument @var{dont-ask} is non-nil, the proof process is terminated
 without confirmation.
 
@@ -2306,11 +2306,13 @@ The size of the ring is set by the variable @code{pg-input-ring-size}.
 
 @c TEXI DOCSTRING MAGIC: pg-previous-input
 @deffn Command pg-previous-input arg
-Cycle backwards through input history, saving input.
+Cycle backwards through input history, saving input.@*
+If called interactively, @var{arg} is given by the prefix argument.
 @end deffn
 @c TEXI DOCSTRING MAGIC: pg-next-input
 @deffn Command pg-next-input arg
-Cycle forwards through input history.
+Cycle forwards through input history.@*
+If called interactively, @var{arg} is given by the prefix argument.
 @end deffn
 @c TEXI DOCSTRING MAGIC: pg-previous-matching-input
 @deffn Command pg-previous-matching-input regexp n
@@ -2685,7 +2687,7 @@ Show a buffer of all the shortcuts available.
 @deffn Command unicode-tokens-list-unicode-chars 
 Insert each Unicode character into a buffer.@*
 Lets you see which characters are available for literal display
-in your emacs font.
+in your Emacs font.
 
 (fn)
 @end deffn
@@ -3467,49 +3469,40 @@ For multiple frame mode, this function obeys the setting of
 
 For single frame mode:
 
-@itemize @bullet
-@item
-In two panes mode, this uses a canonical layout made by splitting
-Emacs windows in equal proportions. The splitting is vertical if
-emacs width is smaller than @samp{@code{split-width-threshold}} and
-horizontal otherwise. You can then adjust the proportions by
+- In two panes mode, this uses a canonical layout made by splitting
+Emacs windows in equal proportions.  The splitting is vertical if
+Emacs width is smaller than @samp{@code{split-width-threshold}} and
+horizontal otherwise.  You can then adjust the proportions by
 dragging the separating bars.
 
-@item
-In three pane mode, there are three display modes, depending
-where the three useful buffers are displayed: scripting
-buffer, goals buffer and response buffer.
-
-Here are the three modes:
-
-@itemize @bullet
-@item
-@code{vertical}: the 3 buffers are displayed in one column.
-
-@item
-@code{hybrid}: 2 columns mode, left column displays scripting buffer
-and right column displays the 2 others.
-
-@item
-@code{horizontal}: 3 columns mode, one for each buffer (script, goals, response).
-@end itemize
-
-By default, the display mode is automatically chosen by
-considering the current emacs frame width: if it is smaller
-than @samp{@code{split-width-threshold}} then vertical mode is chosen,
-otherwise if it is smaller than 1.5 * @samp{@code{split-width-threshold}}
-then hybrid mode is chosen, finally if the frame is larger than
-1.5 * @samp{@code{split-width-threshold}} then the horizontal mode is chosen.
-
-You can change the value of @samp{@code{split-width-threshold}} at your
-will.
-
-If you want to force one of the layouts, you can set variable
-@samp{@code{proof-three-window-mode-policy}} to @code{'vertical}, @code{'horizontal} or
-@code{'hybrid}. The default value is @code{'smart} which sets the automatic
-behaviour described above.
-@end itemize
-
+- In three pane mode, there are three display modes, depending
+@lisp
+  where the three useful buffers are displayed: scripting
+  buffer, goals buffer and response buffer.
+
+  Here are the three modes:
+
+  - vertical: the 3 buffers are displayed in one column.
+  - hybrid: 2 columns mode, left column displays scripting buffer
+    and right column displays the 2 others.
+  - horizontal: 3 columns mode, one for each buffer (script, goals,
+    response).
+
+  By default, the display mode is automatically chosen by
+  considering the current Emacs frame width: if it is smaller
+  than @samp{@code{split-width-threshold}} then vertical mode is chosen,
+  otherwise if it is smaller than 1.5 * @samp{@code{split-width-threshold}}
+  then hybrid mode is chosen, finally if the frame is larger than
+  1.5 * @samp{@code{split-width-threshold}} then the horizontal mode is chosen.
+
+  You can change the value of @samp{@code{split-width-threshold}} at your
+  will.
+
+  If you want to force one of the layouts, you can set variable
+  @samp{@code{proof-three-window-mode-policy}} to @code{'vertical}, @code{'horizontal} or
+  @code{'hybrid}.  The default value is @code{'smart} which sets the automatic
+  behaviour described above.
+@end lisp
 @end deffn
 
 @c TEXI DOCSTRING MAGIC: proof-shrink-windows-tofit
@@ -3537,7 +3530,7 @@ Hovers will be added when this option is non-nil.  Prover outputs
 can be displayed when the mouse hovers over the region that
 produced it and output is available (see @samp{@code{proof-full-annotation}}).
 If output is not available, the type of the output region is displayed.
-Changes of this option will not be reflected in already-processed 
+Changes of this option will not be reflected in already-processed
 regions of the script.
 
 The default value is @code{nil}.
@@ -3762,8 +3755,8 @@ locked (coloured blue); a buffer is completely unprocessed when there
 is no locked region.
 
 For some proof assistants (such as Coq) fully processed buffers make
-no sense. Setting this option to @code{'process} has then the same effect
-as leaving it unset (nil). (This behaviour is controlled by
+no sense.  Setting this option to @code{'process} has then the same effect
+as leaving it unset (nil).  (This behaviour is controlled by
 @samp{@code{proof-no-fully-processed-buffer}}.)
 
 The default value is @code{nil}.
@@ -4427,17 +4420,16 @@ Documentation of the user option @code{coq-project-filename}:
 @c TEXI DOCSTRING MAGIC: coq-project-filename
 @defvar coq-project-filename 
 The name of coq project file.@*
-The coq project file of a coq development (Cf Coq documentation
-on "makefile generation") should contain the arguments given to
+The coq project file of a coq development (cf. Coq documentation on
+"makefile generation") should contain the arguments given to
 coq_makefile. In particular it contains the -I and -R
-options (preferably one per line). If @samp{coq-use-coqproject} is
-t (default) the content of this file will be used by Proof General
-to infer the @samp{@code{coq-load-path}} and the @samp{@code{coq-prog-args}} variables
-that set the coqtop invocation by Proof General. This is now the
-recommended way of configuring the coqtop invocation. Local file
-variables may still be used to override the coq project file's
-configuration. .dir-locals.el files also work and override
-project file settings.
+options (preferably one per line).  If @samp{coq-use-coqproject} is
+t (default) the content of this file will be used by Proof General to
+infer the @samp{@code{coq-load-path}} and the @samp{@code{coq-prog-args}} variables that set
+the coqtop invocation by Proof General.  This is now the recommended
+way of configuring the coqtop invocation.  Local file variables may
+still be used to override the coq project file's configuration.
+.dir-locals.el files also work and override project file settings.
 @end defvar
 
 
@@ -4451,8 +4443,8 @@ down to ``Coq Use Project File'').
 
 @c TEXI DOCSTRING MAGIC: coq-use-project-file
 @defvar coq-use-project-file 
-If t, when opening a coq file read the dominating _CoqProject.@*
-If t, when a coq file is opened, Proof General will look for a
+If t, when opening a Coq file read the dominating _CoqProject.@*
+If t, when a Coq file is opened, Proof General will look for a
 project file (see @samp{@code{coq-project-filename}}) somewhere in the
 current directory or its parent directories.  If there is one,
 its contents are read and used to determine the arguments that
@@ -4891,7 +4883,7 @@ Coq Auto Compile -> Coq Auto Compile}.
 @defvar coq-compile-before-require 
 If non-nil, check dependencies of required modules and compile if necessary.@*
 If non-nil ProofGeneral intercepts "Require" commands and checks if the
-required library module and its dependencies are up-to-date. If not, they
+required library module and its dependencies are up-to-date.  If not, they
 are compiled from the sources before the "Require" command is processed.
 
 This option can be set/reset via menu
@@ -4904,7 +4896,7 @@ This option can be set/reset via menu
 Buffers to save before checking dependencies for compilation.@*
 There are two orthogonal choices: Firstly one can save all or only the coq
 buffers, where coq buffers means all buffers in coq mode except the current
-buffer. Secondly, Emacs can ask about each such buffer or save all of them
+buffer.  Secondly, Emacs can ask about each such buffer or save all of them
 unconditionally.
 
 This makes four permitted values: @code{'ask-coq} to confirm saving all
@@ -4924,12 +4916,12 @@ The following options configure parallel compilation.
 @defvar coq-compile-parallel-in-background 
 Choose the internal compilation method.@*
 When Proof General compiles itself, you have the choice between
-two implementations. If this setting is nil, then Proof General
+two implementations.  If this setting is nil, then Proof General
 uses the old implementation and compiles everything sequentially
-with synchronous job. With this old method Proof General is
-locked during compilation. If this setting is t, then the new
+with synchronous job.  With this old method Proof General is
+locked during compilation.  If this setting is t, then the new
 method is used and compilation jobs are dispatched in parallel in
-the background. The maximal number of parallel compilation jobs
+the background.  The maximal number of parallel compilation jobs
 is set with @samp{@code{coq-max-background-compilation-jobs}}.
 
 This option can be set/reset via menu
@@ -4959,9 +4951,9 @@ This option can be set/reset via menu
 @defvar coq-max-background-compilation-jobs 
 Maximal number of parallel jobs, if parallel compilation is enabled.@*
 Use the number of available CPU cores if this is set to
-@code{'all-cpus}. This variable is the user setting. The value that is
-really used is @samp{@code{coq--internal-max-jobs}}. Use @samp{@code{coq-max-jobs-setter}}
-or the customization system to change this variable. Otherwise
+@code{'all-cpus}.  This variable is the user setting.  The value that is
+really used is @samp{@code{coq--internal-max-jobs}}.  Use @samp{@code{coq-max-jobs-setter}}
+or the customization system to change this variable.  Otherwise
 your change will have no effect, because @samp{@code{coq--internal-max-jobs}}
 is not adapted.
 @end defvar
@@ -4989,7 +4981,7 @@ Locking ancestors can be disabled with the following option.
 @defvar coq-lock-ancestors 
 If non-nil, lock ancestor module files.@*
 If external compilation is used (via @samp{@code{coq-compile-command}}) then
-only the direct ancestors are locked. Otherwise all ancestors are
+only the direct ancestors are locked.  Otherwise all ancestors are
 locked when the "Require" command is processed.
 
 This option can be set via menu
@@ -5005,13 +4997,13 @@ configure the compilation command in @code{coq-compile-command}.
 
 @c TEXI DOCSTRING MAGIC: coq-compile-command
 @defvar coq-compile-command 
-External compilation command. If empty ProofGeneral compiles itself.@*
+External compilation command.  If empty ProofGeneral compiles itself.@*
 If unset (the empty string) ProofGeneral computes the dependencies of
-required modules with coqdep and compiles as necessary. This internal
+required modules with coqdep and compiles as necessary.  This internal
 dependency checking does currently not handle ML modules.
 
 If a non-empty string, the denoted command is called to do the
-dependency checking and compilation. Before executing this
+dependency checking and compilation.  Before executing this
 command the following keys are substituted as follows:
 @lisp
   %p  the (physical) directory containing the source of
@@ -5050,12 +5042,12 @@ configure these things with the following options.
 @defvar coq-load-path 
 Non-standard coq library load path.@*
 This list specifies the LoadPath extension for coqdep, coqc and
-coqtop. Usually, the elements of this list are strings (for
+coqtop.  Usually, the elements of this list are strings (for
 "-I") or lists of two strings (for "-R" dir path and
 "-Q" dir path).
 
 The possible forms of elements of this list correspond to the 4
-forms of include options (@samp{-I} @samp{-Q} and @samp{-R}). An element can be
+forms of include options (@samp{-I} @samp{-Q} and @samp{-R}).  An element can be
 @lisp
   - A list of the form @samp{(}ocamlimport dir)', specifying (in 8.5) a
     directory to be added to ocaml path (@samp{-I}).
@@ -5086,10 +5078,10 @@ not the same (-I is for coq path).
 
 @c TEXI DOCSTRING MAGIC: coq-load-path-include-current
 @defvar coq-load-path-include-current 
-If @samp{t} let coqdep search the current directory too.@*
-Should be @samp{t} for normal users. If @samp{t} pass -Q dir "" to coqdep when
-processing files in directory "dir" in addition to any entries
-in @samp{@code{coq-load-path}}.
+If t, let coqdep search the current directory too.@*
+Should be t for normal users.  If t, pass -Q dir "" to coqdep when
+processing files in directory "dir" in addition to any entries in
+@samp{@code{coq-load-path}}.
 
 This setting is only relevant with Coq < 8.5.
 @end defvar
@@ -5105,12 +5097,12 @@ libraries.
 @defvar coq-compile-ignored-directories 
 Directories in which ProofGeneral should not compile modules.@*
 List of regular expressions for directories in which ProofGeneral
-should not compile modules. If a library file name matches one
+should not compile modules.  If a library file name matches one
 of the regular expressions in this list then ProofGeneral does
 neither compile this file nor check its dependencies for
-compilation. It makes sense to include non-standard coq library
+compilation.  It makes sense to include non-standard coq library
 directories here if they are not changed and if they are so big
-that dependency checking takes noticeable time. The regular
+that dependency checking takes noticeable time.  The regular
 expressions in here are always matched against the .vo file name,
 regardless whether @samp{`-quick}' would be used to compile the file
 or not.
@@ -5737,18 +5729,21 @@ Here are some of the other user options specific to EasyCrypt.  You can
 set these as usual with the customization mechanism.
 
 @c TEXI DOCSTRING MAGIC: easycrypt-prog-name
-@defvar easycrypt-prog-name
+@defopt easycrypt-prog-name 
 Name of program to run EasyCrypt.
-@end defvar
+
+The default value is @code{"easycrypt"}.
+@end defopt
 
 @c TEXI DOCSTRING MAGIC: easycrypt-load-path
-@defvar easycrypt-load-path
-Non-standard EasyCrypt library load path. This list specifies the
-include path for EasyCrypt.
+@defvar easycrypt-load-path 
+Non-standard EasyCrypt library load path.@*
+This list specifies the include path for EasyCrypt.  The elements of
+this list are strings.
 @end defvar
 
 @c TEXI DOCSTRING MAGIC: easycrypt-web-page
-@defvar easycrypt-web-page
+@defvar easycrypt-web-page 
 URL of web page for EasyCrypt.
 @end defvar