diff options
Diffstat (limited to 'generic/proof-script.el')
| -rw-r--r-- | generic/proof-script.el | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/generic/proof-script.el b/generic/proof-script.el index 5b7492a0..5b4a5123 100644 --- a/generic/proof-script.el +++ b/generic/proof-script.el @@ -448,7 +448,7 @@ proof assistant and Emacs is has a modified buffer visiting the file." (buffer (proof-file-to-buffer cfile))) (proof-debug (concat "Registering file " cfile (if (member cfile proof-included-files-list) - " (already registered, no action)." "."))) + " (already registered, no action)" ""))) (unless (member cfile proof-included-files-list) (and buffer (not informprover) @@ -543,7 +543,7 @@ retracted using proof-auto-retract-dependencies." (concat "Unregistering file " cfile (if (not (member cfile proof-included-files-list)) - " (not registered, no action)." "."))) + " (not registered, no action)" ""))) (if (member cfile proof-included-files-list) (progn (proof-auto-retract-dependencies cfile informprover) @@ -1897,9 +1897,9 @@ This is intended as a value for proof-activate-scripting-hook" ;; (proof-define-assistant-command-witharg proof-find-theorems - "Search for items containing a given constant." + "Search for items containing given constants." proof-find-theorems-command - "Find theorems containing the constant" + "Find theorems containing the constant(s)" (proof-shell-invisible-command arg)) (proof-define-assistant-command-witharg proof-issue-goal |