diff options
Diffstat (limited to 'generic')
| -rw-r--r-- | generic/proof-config.el | 8 | ||||
| -rw-r--r-- | generic/proof-script.el | 6 | ||||
| -rw-r--r-- | generic/proof-toolbar.el | 2 |
3 files changed, 8 insertions, 8 deletions
diff --git a/generic/proof-config.el b/generic/proof-config.el index aab2e4d6..2a563855 100644 --- a/generic/proof-config.el +++ b/generic/proof-config.el @@ -437,17 +437,17 @@ command line options. For an example, see coq/coq.el." :type 'string :group 'prover-config) -(defcustom proof-ctxt-string "" +(defcustom proof-context-command "" "Command to display the context in proof assistant." :type 'string :group 'prover-config) -(defcustom proof-help-string "" - "Command to ask for help in proof assistant." +(defcustom proof-info-command "" + "Command to ask for help or information in the proof assistant." :type 'string :group 'prover-config) -(defcustom proof-prf-string "" +(defcustom proof-proof-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 e6938743..a3f0498e 100644 --- a/generic/proof-script.el +++ b/generic/proof-script.el @@ -1510,14 +1510,14 @@ Start up the proof assistant if necessary." (proof-define-assistant-command proof-prf "Show the current proof state." - proof-prf-string) + proof-proof-command) (proof-define-assistant-command proof-ctxt "Show the current context." - proof-ctxt-string) + proof-context-command) (proof-define-assistant-command proof-help "Show a help or information message from the proof assistant. Typically, a list of syntax of commands available." - proof-help-string) + proof-info-command) ;; ;; Commands which require an argument, and maybe affect the script. diff --git a/generic/proof-toolbar.el b/generic/proof-toolbar.el index 3051764d..805c0dfb 100644 --- a/generic/proof-toolbar.el +++ b/generic/proof-toolbar.el @@ -27,7 +27,7 @@ ;; in proof-toolbar-setup. ;; FIXME: consider automatically disabling buttons which are -;; not configured for the prover, e.g. if proof-help-string is +;; not configured for the prover, e.g. if proof-info-command is ;; not set, then the Info button should not be show. ;; FIXME: In the future, add back the enabler functions. |