diff options
| author | David Aspinall | 1999-10-01 18:36:01 +0000 |
|---|---|---|
| committer | David Aspinall | 1999-10-01 18:36:01 +0000 |
| commit | 275d38ca5a77ae960504ce9af55d4c0cdf9174d6 (patch) | |
| tree | cc057ba43348afa39c0e0b434cd04672d616fa35 | |
| parent | 45b27c9fcc1461f43ccf1c65f8e3f55b6426b8d1 (diff) | |
Fixup name changes
| -rw-r--r-- | doc/ProofGeneral.texi | 20 | ||||
| -rw-r--r-- | generic/proof-config.el | 2 | ||||
| -rw-r--r-- | generic/proof-script.el | 2 |
3 files changed, 12 insertions, 12 deletions
diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi index f302e650..eca6b32f 100644 --- a/doc/ProofGeneral.texi +++ b/doc/ProofGeneral.texi @@ -1133,20 +1133,20 @@ from a proof script. Here are the keybindings and functions. @c TEXI DOCSTRING MAGIC: proof-prf @deffn Command proof-prf Show the current proof state.@* -Issues a command to the assistant from @code{proof-prf-string}. +Issues a command to the assistant from @code{proof-showproof-command}. @end deffn @c TEXI DOCSTRING MAGIC: proof-ctxt @deffn Command proof-ctxt Show the current context.@* -Issues a command to the assistant from @code{proof-ctxt-string}. +Issues a command to the assistant from @code{proof-context-command}. @end deffn @c TEXI DOCSTRING MAGIC: proof-help @deffn Command proof-help Show a help or information message from the proof assistant.@* Typically, a list of syntax of commands available. -Issues a command to the assistant from @code{proof-help-string}. +Issues a command to the assistant from @code{proof-info-command}. @end deffn @c TEXI DOCSTRING MAGIC: proof-interrupt-process @@ -2451,16 +2451,16 @@ Suggestion: this can be set in the script mode configuration. @defvar proof-assistant-home-page Web address for information on proof assistant @end defvar -@c TEXI DOCSTRING MAGIC: proof-ctxt-string -@defvar proof-ctxt-string +@c TEXI DOCSTRING MAGIC: proof-context-command +@defvar proof-context-command Command to display the context in proof assistant. @end defvar -@c TEXI DOCSTRING MAGIC: proof-help-string -@defvar proof-help-string -Command to ask for help in proof assistant. +@c TEXI DOCSTRING MAGIC: proof-info-command +@defvar proof-info-command +Command to ask for help or information in the proof assistant. @end defvar -@c TEXI DOCSTRING MAGIC: proof-prf-string -@defvar proof-prf-string +@c TEXI DOCSTRING MAGIC: proof-showproof-command +@defvar proof-showproof-command Command to display proof state in proof assistant. @end defvar @c TEXI DOCSTRING MAGIC: proof-goal-command diff --git a/generic/proof-config.el b/generic/proof-config.el index 2a563855..72c6d3cc 100644 --- a/generic/proof-config.el +++ b/generic/proof-config.el @@ -447,7 +447,7 @@ command line options. For an example, see coq/coq.el." :type 'string :group 'prover-config) -(defcustom proof-proof-command "" +(defcustom proof-showproof-command "" "Command to display proof state in proof assistant." :type 'string :group 'prover-config) diff --git a/generic/proof-script.el b/generic/proof-script.el index a3f0498e..231368cb 100644 --- a/generic/proof-script.el +++ b/generic/proof-script.el @@ -1510,7 +1510,7 @@ Start up the proof assistant if necessary." (proof-define-assistant-command proof-prf "Show the current proof state." - proof-proof-command) + proof-showproof-command) (proof-define-assistant-command proof-ctxt "Show the current context." proof-context-command) |
