Run make autoloads

1 files changed, 135 insertions, 129 deletions

diff --git a/generic/proof-autoloads.el b/generic/proof-autoloads.el
index e93c4da2..67904203 100644
--- a/generic/proof-autoloads.el
+++ b/generic/proof-autoloads.el
@@ -28,11 +28,11 @@
 (provide 'proof-autoloads)
 
 
-;;;### (autoloads (bufhist-exit bufhist-init bufhist-mode) "bufhist"
-;;;;;;  "../lib/bufhist.el" (20118 50210))
+;;;### (autoloads nil "../lib/bufhist" "../lib/bufhist.el" (23421
+;;;;;;  61555 968003 660000))
 ;;; Generated autoloads from ../lib/bufhist.el
 
-(autoload 'bufhist-mode "bufhist" "\
+(autoload 'bufhist-mode "../lib/bufhist" "\
 Minor mode retaining an in-memory history of the buffer contents.
 
 Commands:\\<bufhist-minor-mode-map>
@@ -45,32 +45,31 @@ Commands:\\<bufhist-minor-mode-map>
 
 \(fn &optional ARG)" t nil)
 
-(autoload 'bufhist-init "bufhist" "\
+(autoload 'bufhist-init "../lib/bufhist" "\
 Initialise a ring history for the current buffer.
 The history will be read-only unless READWRITE is non-nil.
 For read-only histories, edits to the buffer switch to the latest version.
-The size defaults to `bufhist-ring-size'.
+If RINGSIZE is omitted or nil, the size defaults to ‘bufhist-ring-size’.
 
 \(fn &optional READWRITE RINGSIZE)" t nil)
 
-(autoload 'bufhist-exit "bufhist" "\
+(autoload 'bufhist-exit "../lib/bufhist" "\
 Stop keeping ring history for current buffer.
 
 \(fn)" t nil)
 
 ;;;***
 
-;;;### (autoloads (holes-insert-and-expand holes-abbrev-complete
-;;;;;;  holes-mode holes-set-make-active-hole) "holes" "../lib/holes.el"
-;;;;;;  (20118 50210))
+;;;### (autoloads nil "../lib/holes" "../lib/holes.el" (23421 61555
+;;;;;;  968003 660000))
 ;;; Generated autoloads from ../lib/holes.el
 
-(autoload 'holes-set-make-active-hole "holes" "\
+(autoload 'holes-set-make-active-hole "../lib/holes" "\
 Make a new hole between START and END or at point, and make it active.
 
 \(fn &optional START END)" t nil)
 
-(autoload 'holes-mode "holes" "\
+(autoload 'holes-mode "../lib/holes" "\
 Toggle Holes minor mode.
 With arg, turn Outline minor mode on if arg is positive, off otherwise.
 
@@ -160,7 +159,7 @@ undoing on holes cannot make holes re-appear.
 
 \(fn &optional ARG)" t nil)
 
-(autoload 'holes-abbrev-complete "holes" "\
+(autoload 'holes-abbrev-complete "../lib/holes" "\
 Complete abbrev by putting holes and indenting.
 Moves point at beginning of expanded text.  Put this function as
 call-back for your abbrevs, and just expanded \"#\" and \"@{..}\" will
@@ -168,18 +167,18 @@ become holes.
 
 \(fn)" nil nil)
 
-(autoload 'holes-insert-and-expand "holes" "\
+(autoload 'holes-insert-and-expand "../lib/holes" "\
 Insert S, expand it and replace #s and @{]s by holes.
 
 \(fn S)" nil nil)
 
 ;;;***
 
-;;;### (autoloads (maths-menu-mode) "maths-menu" "../lib/maths-menu.el"
-;;;;;;  (20118 50210))
+;;;### (autoloads nil "../lib/maths-menu" "../lib/maths-menu.el"
+;;;;;;  (23421 61555 968003 660000))
 ;;; Generated autoloads from ../lib/maths-menu.el
 
-(autoload 'maths-menu-mode "maths-menu" "\
+(autoload 'maths-menu-mode "../lib/maths-menu" "\
 Install a menu for entering mathematical characters.
 Uses window system menus only when they can display multilingual text.
 Otherwise the menu-bar item activates the text-mode menu system.
@@ -189,8 +188,8 @@ This mode is only useful with a font which can display the maths repertoire.
 
 ;;;***
 
-;;;### (autoloads (proof-associated-windows proof-associated-buffers)
-;;;;;;  "pg-assoc" "pg-assoc.el" (20118 50210))
+;;;### (autoloads nil "pg-assoc" "pg-assoc.el" (23421 61555 964003
+;;;;;;  698000))
 ;;; Generated autoloads from pg-assoc.el
 
 (autoload 'proof-associated-buffers "pg-assoc" "\
@@ -201,25 +200,32 @@ Some may be dead/nil.
 
 (autoload 'proof-associated-windows "pg-assoc" "\
 Return a list of the associated buffers windows.
-Dead or nil buffers are not represented in the list.
+Dead or nil buffers are not represented in the list.  Optional
+argument ALL-FRAMES has the same meaning than for
+`get-buffer-window'.
+
+\(fn &optional ALL-FRAMES)" nil nil)
+
+(autoload 'proof-associated-frames "pg-assoc" "\
+Return the list of frames displaying at least one associated buffer.
 
 \(fn)" nil nil)
 
 ;;;***
 
-;;;### (autoloads (profile-pg) "pg-dev" "../lib/pg-dev.el" (20118
-;;;;;;  50210))
+;;;### (autoloads nil "../lib/pg-dev" "../lib/pg-dev.el" (23421 61555
+;;;;;;  968003 660000))
 ;;; Generated autoloads from ../lib/pg-dev.el
 
-(autoload 'profile-pg "pg-dev" "\
-Configure Proof General for profiling.  Use M-x elp-results to see results.
+(autoload 'profile-pg "../lib/pg-dev" "\
+Configure Proof General for profiling.  Use \\[elp-results] to see results.
 
 \(fn)" t nil)
 
 ;;;***
 
-;;;### (autoloads (proof-goals-config-done) "pg-goals" "pg-goals.el"
-;;;;;;  (20118 50210))
+;;;### (autoloads nil "pg-goals" "pg-goals.el" (23421 61555 964003
+;;;;;;  698000))
 ;;; Generated autoloads from pg-goals.el
 
 (autoload 'proof-goals-config-done "pg-goals" "\
@@ -229,8 +235,8 @@ Initialise the goals buffer after the child has been configured.
 
 ;;;***
 
-;;;### (autoloads (pg-movie-export-directory pg-movie-export-from
-;;;;;;  pg-movie-export) "pg-movie" "pg-movie.el" (20123 64158))
+;;;### (autoloads nil "pg-movie" "pg-movie.el" (23421 61555 964003
+;;;;;;  698000))
 ;;; Generated autoloads from pg-movie.el
 
 (autoload 'pg-movie-export "pg-movie" "\
@@ -252,8 +258,8 @@ Existing XML files are overwritten.
 
 ;;;***
 
-;;;### (autoloads (defpacustom proof-defpacustom-fn) "pg-pamacs"
-;;;;;;  "pg-pamacs.el" (20118 50210))
+;;;### (autoloads nil "pg-pamacs" "pg-pamacs.el" (23421 61555 964003
+;;;;;;  698000))
 ;;; Generated autoloads from pg-pamacs.el
 
 (autoload 'proof-defpacustom-fn "pg-pamacs" "\
@@ -269,7 +275,9 @@ which can be changed by sending commands.
 In this case, NAME stands for the internal setting, flag, etc,
 for the proof assistant, and a :setting and :type value should be
 provided.  The :type of NAME should be one of 'integer, 'float,
-'boolean, 'string.
+'boolean, 'string.  Other types are not supported (see
+`proof-menu-entry-for-setting').  They will yield an error when
+constructing the proof assistant menu.
 
 The function `proof-assistant-format' is used to format VAL.
 
@@ -297,12 +305,12 @@ Additional properties in the ARGS prop list may include:
 
 This macro also extends the `proof-assistant-settings' list.
 
-\(fn NAME VAL &rest ARGS)" nil (quote macro))
+\(fn NAME VAL &rest ARGS)" nil t)
 
 ;;;***
 
-;;;### (autoloads (pg-pgip-askprefs pg-pgip-maybe-askpgip pg-pgip-process-packet)
-;;;;;;  "pg-pgip" "pg-pgip.el" (20123 64607))
+;;;### (autoloads nil "pg-pgip" "pg-pgip.el" (23421 61555 964003
+;;;;;;  698000))
 ;;; Generated autoloads from pg-pgip.el
 
 (autoload 'pg-pgip-process-packet "pg-pgip" "\
@@ -323,10 +331,8 @@ Send an <askprefs> message to the prover.
 
 ;;;***
 
-;;;### (autoloads (pg-response-has-error-location proof-next-error
-;;;;;;  pg-response-message pg-response-display-with-face pg-response-maybe-erase
-;;;;;;  proof-response-config-done proof-response-mode) "pg-response"
-;;;;;;  "pg-response.el" (20118 50210))
+;;;### (autoloads nil "pg-response" "pg-response.el" (23421 61555
+;;;;;;  964003 698000))
 ;;; Generated autoloads from pg-response.el
 
 (autoload 'proof-response-mode "pg-response" "\
@@ -340,18 +346,31 @@ Complete initialisation of a response-mode derived buffer.
 \(fn)" nil nil)
 
 (autoload 'pg-response-maybe-erase "pg-response" "\
-Erase the response buffer according to `pg-response-erase-flag'.
+Erase the response buffer, according to confusing flag combinations.
+
+Mainly, we look at `pg-response-erase-flag' and clear the
+response buffer if this is non-nil, but NOT the special
+symbol 'invisible.
+
 ERASE-NEXT-TIME is the new value for the flag.
-If CLEAN-WINDOWS is set, use `proof-clean-buffer' to do the erasing.
-If FORCE, override `pg-response-erase-flag'.
 
-If the user option `proof-tidy-response' is nil, then
-the buffer is only cleared when FORCE is set.
+FORCE overrides the flag to force cleaning.
+
+KEEP overrides the flag to prevent cleaning.
+
+FORCE takes precedent over KEEP.
+
+If CLEAN-WINDOWS is set, use `proof-clean-buffer' to do the erasing,
+otherwise we use `bufhist-checkpoint-and-erase' to record an
+undo history entry for the current buffer contents.
+
+If the user option `proof-tidy-response' is nil, the buffer
+will never be cleared unless FORCE is set.
 
 No effect if there is no response buffer currently.
 Returns non-nil if response buffer was cleared.
 
-\(fn &optional ERASE-NEXT-TIME CLEAN-WINDOWS FORCE)" nil nil)
+\(fn &optional ERASE-NEXT-TIME CLEAN-WINDOWS FORCE KEEP)" nil nil)
 
 (autoload 'pg-response-display-with-face "pg-response" "\
 Display STR with FACE in response buffer.
@@ -382,20 +401,14 @@ See `pg-next-error-regexp'.
 
 ;;;***
 
-;;;### (autoloads (proof-autosend-enable pg-clear-input-ring pg-remove-from-input-history
-;;;;;;  pg-add-to-input-history pg-next-matching-input-from-input
-;;;;;;  pg-previous-matching-input-from-input proof-imenu-enable
-;;;;;;  pg-identifier-near-point-query pg-hint pg-next-error-hint
-;;;;;;  pg-processing-complete-hint pg-jump-to-end-hint pg-response-buffers-hint
-;;;;;;  pg-slow-fontify-tracing-hint proof-electric-terminator-enable
-;;;;;;  proof-define-assistant-command-witharg proof-define-assistant-command
-;;;;;;  proof-process-buffer proof-goto-point proof-script-new-command-advance)
-;;;;;;  "pg-user" "pg-user.el" (20123 64158))
+;;;### (autoloads nil "pg-user" "pg-user.el" (23421 61555 964003
+;;;;;;  698000))
 ;;; Generated autoloads from pg-user.el
 
 (autoload 'proof-script-new-command-advance "pg-user" "\
-Move point to a nice position for a new command.
+Move point to a nice position for a new command, possibly inserting spaces.
 Assumes that point is at the end of a command.
+No effect if `proof-next-command-insert-space' is nil.
 
 \(fn)" t nil)
 
@@ -412,35 +425,37 @@ Process the current (or script) buffer, and maybe move point to the end.
 \(fn)" t nil)
 
 (autoload 'proof-define-assistant-command "pg-user" "\
-Define FN (docstring DOC) to send BODY to prover, based on CMDVAR.
+Define FN (docstring DOC): check if CMDVAR is set, then send BODY to prover.
 BODY defaults to CMDVAR, a variable.
 
-\(fn FN DOC CMDVAR &optional BODY)" nil (quote macro))
+\(fn FN DOC CMDVAR &optional BODY)" nil t)
 
 (autoload 'proof-define-assistant-command-witharg "pg-user" "\
-Define command FN to prompt for string CMDVAR to proof assistant.
+Define FN (arg) with DOC: check CMDVAR is set, PROMPT a string and eval BODY.
+The BODY can contain occurrences of arg.
 CMDVAR is a variable holding a function or string.  Automatically has history.
 
-\(fn FN DOC CMDVAR PROMPT &rest BODY)" nil (quote macro))
+\(fn FN DOC CMDVAR PROMPT &rest BODY)" nil t)
 
 (autoload 'proof-electric-terminator-enable "pg-user" "\
 Ensure modeline update to display new value for electric terminator.
 This a function is called by the custom-set property 'proof-set-value.
+It can also be used as a minor mode function: with ARG, turn on iff ARG>0
 
-\(fn)" nil nil)
+\(fn &optional ARG)" nil nil)
 
 (autoload 'pg-slow-fontify-tracing-hint "pg-user" "\
-Not documented
+
 
 \(fn)" nil nil)
 
 (autoload 'pg-response-buffers-hint "pg-user" "\
-Not documented
+
 
 \(fn &optional NEXTBUF)" nil nil)
 
 (autoload 'pg-jump-to-end-hint "pg-user" "\
-Not documented
+
 
 \(fn)" nil nil)
 
@@ -503,7 +518,7 @@ removed if it matches the last item in the ring.
 \(fn CMD)" nil nil)
 
 (autoload 'pg-clear-input-ring "pg-user" "\
-Not documented
+
 
 \(fn)" nil nil)
 
@@ -514,8 +529,7 @@ Enable or disable autosend behaviour.
 
 ;;;***
 
-;;;### (autoloads (pg-xml-parse-string) "pg-xml" "pg-xml.el" (20118
-;;;;;;  50210))
+;;;### (autoloads nil "pg-xml" "pg-xml.el" (23421 61555 964003 698000))
 ;;; Generated autoloads from pg-xml.el
 
 (autoload 'pg-xml-parse-string "pg-xml" "\
@@ -525,8 +539,8 @@ Parse string in ARG, same as pg-xml-parse-buffer.
 
 ;;;***
 
-;;;### (autoloads (proof-dependency-in-span-context-menu proof-depends-process-dependencies)
-;;;;;;  "proof-depends" "proof-depends.el" (20118 50210))
+;;;### (autoloads nil "proof-depends" "proof-depends.el" (23421 61555
+;;;;;;  964003 698000))
 ;;; Generated autoloads from proof-depends.el
 
 (autoload 'proof-depends-process-dependencies "proof-depends" "\
@@ -543,21 +557,22 @@ Make some menu entries showing proof dependencies of SPAN.
 
 ;;;***
 
-;;;### (autoloads (proof-easy-config) "proof-easy-config" "proof-easy-config.el"
-;;;;;;  (20118 50210))
+;;;### (autoloads nil "proof-easy-config" "proof-easy-config.el"
+;;;;;;  (23421 61555 964003 698000))
 ;;; Generated autoloads from proof-easy-config.el
 
 (autoload 'proof-easy-config "proof-easy-config" "\
-Configure Proof General for proof-assistant using BODY as a setq body.
+Configure Proof General for a given proof assistant.
 The symbol SYM and string name NAME must match those given in
-the `proof-assistant-table', which see.
+  the `proof-assistant-table', which see.
+Additional arguments are taken into account as a setq BODY.
 
-\(fn SYM NAME &rest BODY)" nil (quote macro))
+\(fn SYM NAME &rest BODY)" nil t)
 
 ;;;***
 
-;;;### (autoloads (proof-indent-line) "proof-indent" "proof-indent.el"
-;;;;;;  (20118 50210))
+;;;### (autoloads nil "proof-indent" "proof-indent.el" (23421 34760
+;;;;;;  554828 678000))
 ;;; Generated autoloads from proof-indent.el
 
 (autoload 'proof-indent-line "proof-indent" "\
@@ -567,8 +582,8 @@ Indent current line of proof script, if indentation enabled.
 
 ;;;***
 
-;;;### (autoloads (proof-maths-menu-enable proof-maths-menu-set-global)
-;;;;;;  "proof-maths-menu" "proof-maths-menu.el" (20118 50210))
+;;;### (autoloads nil "proof-maths-menu" "proof-maths-menu.el" (23421
+;;;;;;  34760 554828 678000))
 ;;; Generated autoloads from proof-maths-menu.el
 
 (autoload 'proof-maths-menu-set-global "proof-maths-menu" "\
@@ -588,9 +603,8 @@ in future if we have just activated it for this buffer.
 
 ;;;***
 
-;;;### (autoloads (proof-aux-menu proof-menu-define-specific proof-menu-define-main
-;;;;;;  proof-menu-define-keys) "proof-menu" "proof-menu.el" (20123
-;;;;;;  63408))
+;;;### (autoloads nil "proof-menu" "proof-menu.el" (23421 61555 964003
+;;;;;;  698000))
 ;;; Generated autoloads from proof-menu.el
 
 (autoload 'proof-menu-define-keys "proof-menu" "\
@@ -599,12 +613,12 @@ Prover specific keymap under C-c C-a.
 \(fn MAP)" nil nil)
 
 (autoload 'proof-menu-define-main "proof-menu" "\
-Not documented
+
 
 \(fn)" nil nil)
 
 (autoload 'proof-menu-define-specific "proof-menu" "\
-Not documented
+
 
 \(fn)" nil nil)
 
@@ -615,12 +629,8 @@ Construct and return PG auxiliary menu used in non-scripting buffers.
 
 ;;;***
 
-;;;### (autoloads (proof-config-done proof-mode proof-insert-sendback-command
-;;;;;;  proof-insert-pbp-command proof-script-generic-parse-find-comment-end
-;;;;;;  proof-register-possibly-new-processed-file pg-set-span-helphighlights
-;;;;;;  proof-locked-region-empty-p proof-locked-region-full-p proof-unprocessed-begin
-;;;;;;  proof-colour-locked) "proof-script" "proof-script.el" (20123
-;;;;;;  64988))
+;;;### (autoloads nil "proof-script" "proof-script.el" (23421 61555
+;;;;;;  964003 698000))
 ;;; Generated autoloads from proof-script.el
 
 (autoload 'proof-colour-locked "proof-script" "\
@@ -709,11 +719,8 @@ finish setup which depends on specific proof assistant configuration.
 
 ;;;***
 
-;;;### (autoloads (proof-shell-config-done proof-shell-mode proof-shell-invisible-command-invisible-result
-;;;;;;  proof-shell-invisible-cmd-get-result proof-shell-invisible-command
-;;;;;;  proof-shell-wait proof-extend-queue proof-start-queue proof-shell-insert
-;;;;;;  proof-shell-available-p proof-shell-ready-prover) "proof-shell"
-;;;;;;  "proof-shell.el" (20118 50320))
+;;;### (autoloads nil "proof-shell" "proof-shell.el" (23421 61555
+;;;;;;  964003 698000))
 ;;; Generated autoloads from proof-shell.el
 
 (autoload 'proof-shell-ready-prover "proof-shell" "\
@@ -726,7 +733,7 @@ No change to current buffer or point.
 \(fn &optional QUEUEMODE)" nil nil)
 
 (defsubst proof-shell-live-buffer nil "\
-Return non-nil if proof-shell-buffer is live." (and proof-shell-buffer (buffer-live-p proof-shell-buffer) (scomint-check-proc proof-shell-buffer)))
+Return non-nil if ‘proof-shell-buffer’ is live." (and proof-shell-buffer (buffer-live-p proof-shell-buffer) (scomint-check-proc proof-shell-buffer)))
 
 (autoload 'proof-shell-available-p "proof-shell" "\
 Return non-nil if there is a proof shell active and available.
@@ -743,9 +750,9 @@ single string.
 The ACTION argument is a symbol which is typically the name of a
 callback for when each string has been processed.
 
-This calls `proof-shell-insert-hook'.  The arguments `action' and
-`scriptspan' may be examined by the hook to determine how to modify
-the `string' variable (exploiting dynamic scoping) which will be
+This calls `proof-shell-insert-hook'.  The arguments ACTION and
+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
@@ -762,11 +769,11 @@ used in `proof-add-to-queue' when we start processing a queue, and in
 \(fn STRINGS ACTION &optional SCRIPTSPAN)" nil nil)
 
 (autoload 'proof-start-queue "proof-shell" "\
-Begin processing a queue of commands in QUEUEITEMS.
+Begin processing a queue of commands.
 If START is non-nil, START and END are buffer positions in the
 active scripting buffer for the queue region.
 
-This function calls `proof-add-to-queue'.
+This function calls ‘proof-add-to-queue’ with args QUEUEITEMS and QUEUEMODE.
 
 \(fn START END QUEUEITEMS &optional QUEUEMODE)" nil nil)
 
@@ -846,8 +853,8 @@ processing.
 
 ;;;***
 
-;;;### (autoloads (proof-ready-for-assistant) "proof-site" "proof-site.el"
-;;;;;;  (20119 3136))
+;;;### (autoloads nil "proof-site" "proof-site.el" (23421 61555 964003
+;;;;;;  698000))
 ;;; Generated autoloads from proof-site.el
 
 (autoload 'proof-ready-for-assistant "proof-site" "\
@@ -858,8 +865,8 @@ If ASSISTANT-NAME is omitted, look up in `proof-assistant-table'.
 
 ;;;***
 
-;;;### (autoloads (proof-splash-message proof-splash-display-screen)
-;;;;;;  "proof-splash" "proof-splash.el" (20123 63408))
+;;;### (autoloads nil "proof-splash" "proof-splash.el" (23421 61555
+;;;;;;  968003 660000))
 ;;; Generated autoloads from proof-splash.el
 
 (autoload 'proof-splash-display-screen "proof-splash" "\
@@ -877,12 +884,12 @@ Make sure the user gets welcomed one way or another.
 
 ;;;***
 
-;;;### (autoloads (proof-format) "proof-syntax" "proof-syntax.el"
-;;;;;;  (20118 50210))
+;;;### (autoloads nil "proof-syntax" "proof-syntax.el" (23421 61555
+;;;;;;  968003 660000))
 ;;; Generated autoloads from proof-syntax.el
 
 (defsubst proof-replace-regexp-in-string (regexp rep string) "\
-Like replace-regexp-in-string, but set case-fold-search to proof-case-fold-search." (let ((case-fold-search proof-case-fold-search)) (replace-regexp-in-string regexp rep string)))
+Like ‘replace-regexp-in-string’, but set ‘case-fold-search’ to ‘proof-case-fold-search’." (let ((case-fold-search proof-case-fold-search)) (replace-regexp-in-string regexp rep string)))
 
 (autoload 'proof-format "proof-syntax" "\
 Format a string by matching regexps in ALIST against STRING.
@@ -893,8 +900,8 @@ may be a string or sexp evaluated to get a string.
 
 ;;;***
 
-;;;### (autoloads (proof-toolbar-scripting-menu proof-toolbar-setup)
-;;;;;;  "proof-toolbar" "proof-toolbar.el" (20118 50210))
+;;;### (autoloads nil "proof-toolbar" "proof-toolbar.el" (23421 34760
+;;;;;;  554828 678000))
 ;;; Generated autoloads from proof-toolbar.el
 
 (autoload 'proof-toolbar-setup "proof-toolbar" "\
@@ -912,9 +919,8 @@ Menu made from the Proof General toolbar commands.
 
 ;;;***
 
-;;;### (autoloads (proof-unicode-tokens-enable proof-unicode-tokens-set-global
-;;;;;;  proof-unicode-tokens-mode-if-enabled) "proof-unicode-tokens"
-;;;;;;  "proof-unicode-tokens.el" (20118 50210))
+;;;### (autoloads nil "proof-unicode-tokens" "proof-unicode-tokens.el"
+;;;;;;  (23421 34760 554828 678000))
 ;;; Generated autoloads from proof-unicode-tokens.el
 
 (autoload 'proof-unicode-tokens-mode-if-enabled "proof-unicode-tokens" "\
@@ -941,8 +947,8 @@ is changed.
 
 ;;;***
 
-;;;### (autoloads (proof-debug) "proof-utils" "proof-utils.el" (20118
-;;;;;;  50210))
+;;;### (autoloads nil "proof-utils" "proof-utils.el" (23421 61555
+;;;;;;  968003 660000))
 ;;; Generated autoloads from proof-utils.el
 
 (autoload 'proof-debug "proof-utils" "\
@@ -953,11 +959,11 @@ If flag `proof-general-debug' is nil, do nothing.
 
 ;;;***
 
-;;;### (autoloads (scomint-make scomint-make-in-buffer) "scomint"
-;;;;;;  "../lib/scomint.el" (20123 63408))
+;;;### (autoloads nil "../lib/scomint" "../lib/scomint.el" (23421
+;;;;;;  61555 968003 660000))
 ;;; Generated autoloads from ../lib/scomint.el
 
-(autoload 'scomint-make-in-buffer "scomint" "\
+(autoload 'scomint-make-in-buffer "../lib/scomint" "\
 Make a Comint process NAME in BUFFER, running PROGRAM.
 If BUFFER is nil, it defaults to NAME surrounded by `*'s.
 PROGRAM should be either a string denoting an executable program to create
@@ -966,11 +972,11 @@ a TCP connection to be opened via `open-network-stream'.  If there is already
 a running process in that buffer, it is not restarted.  Optional fourth arg
 STARTFILE is the name of a file to send the contents of to the process.
 
-If PROGRAM is a string, any more args are arguments to PROGRAM.
+If PROGRAM is a string, the remaining SWITCHES are arguments to PROGRAM.
 
 \(fn NAME BUFFER PROGRAM &optional STARTFILE &rest SWITCHES)" nil nil)
 
-(autoload 'scomint-make "scomint" "\
+(autoload 'scomint-make "../lib/scomint" "\
 Make a Comint process NAME in a buffer, running PROGRAM.
 The name of the buffer is made by surrounding NAME with `*'s.
 PROGRAM should be either a string denoting an executable program to create
@@ -979,17 +985,17 @@ a TCP connection to be opened via `open-network-stream'.  If there is already
 a running process in that buffer, it is not restarted.  Optional third arg
 STARTFILE is the name of a file to send the contents of the process to.
 
-If PROGRAM is a string, any more args are arguments to PROGRAM.
+If PROGRAM is a string, the remaining SWITCHES are arguments to PROGRAM.
 
 \(fn NAME PROGRAM &optional STARTFILE &rest SWITCHES)" nil nil)
 
 ;;;***
 
-;;;### (autoloads (texi-docstring-magic) "texi-docstring-magic" "../lib/texi-docstring-magic.el"
-;;;;;;  (20118 50210))
+;;;### (autoloads nil "../lib/texi-docstring-magic" "../lib/texi-docstring-magic.el"
+;;;;;;  (23421 61555 968003 660000))
 ;;; Generated autoloads from ../lib/texi-docstring-magic.el
 
-(autoload 'texi-docstring-magic "texi-docstring-magic" "\
+(autoload 'texi-docstring-magic "../lib/texi-docstring-magic" "\
 Update all texi docstring magic annotations in buffer.
 With prefix arg, no errors on unknown symbols.  (This results in
 @def .. @end being deleted if not known).
@@ -998,24 +1004,24 @@ With prefix arg, no errors on unknown symbols.  (This results in
 
 ;;;***
 
-;;;### (autoloads (unicode-chars-list-chars) "unicode-chars" "../lib/unicode-chars.el"
-;;;;;;  (20118 50210))
+;;;### (autoloads nil "../lib/unicode-chars" "../lib/unicode-chars.el"
+;;;;;;  (23421 61555 968003 660000))
 ;;; Generated autoloads from ../lib/unicode-chars.el
 
-(autoload 'unicode-chars-list-chars "unicode-chars" "\
+(autoload 'unicode-chars-list-chars "../lib/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)" t nil)
 
 ;;;***
 
-;;;### (autoloads (unicode-tokens-encode-str) "unicode-tokens" "../lib/unicode-tokens.el"
-;;;;;;  (20118 50210))
+;;;### (autoloads nil "../lib/unicode-tokens" "../lib/unicode-tokens.el"
+;;;;;;  (23421 61555 968003 660000))
 ;;; Generated autoloads from ../lib/unicode-tokens.el
 
-(autoload 'unicode-tokens-encode-str "unicode-tokens" "\
+(autoload 'unicode-tokens-encode-str "../lib/unicode-tokens" "\
 Return a unicode encoded version presentation of STR.
 
 \(fn STR)" nil nil)
@@ -1025,8 +1031,8 @@ Return a unicode encoded version presentation of STR.
 ;;;### (autoloads nil nil ("../lib/local-vars-list.el" "../lib/pg-fontsets.el"
 ;;;;;;  "../lib/proof-compat.el" "../lib/span.el" "pg-autotest.el"
 ;;;;;;  "pg-custom.el" "pg-pbrpm.el" "pg-vars.el" "proof-auxmodes.el"
-;;;;;;  "proof-config.el" "proof-faces.el" "proof-useropts.el" "proof.el"
-;;;;;;  "proofgeneral-pkg.el") (20123 65399 608731))
+;;;;;;  "proof-config.el" "proof-faces.el" "proof-tree.el" "proof-useropts.el"
+;;;;;;  "proof.el") (23421 61555 968003 660000))
 
 ;;;***