aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorDavid Aspinall1999-10-01 18:36:01 +0000
committerDavid Aspinall1999-10-01 18:36:01 +0000
commit275d38ca5a77ae960504ce9af55d4c0cdf9174d6 (patch)
treecc057ba43348afa39c0e0b434cd04672d616fa35
parent45b27c9fcc1461f43ccf1c65f8e3f55b6426b8d1 (diff)
Fixup name changes
-rw-r--r--doc/ProofGeneral.texi20
-rw-r--r--generic/proof-config.el2
-rw-r--r--generic/proof-script.el2
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)