Fix keybinding for completion. Add completion to menubar.

1 files changed, 2 insertions, 1 deletions

diff --git a/generic/proof-menu.el b/generic/proof-menu.el
index f62c3980..5cacdd96 100644
--- a/generic/proof-menu.el
+++ b/generic/proof-menu.el
@@ -46,7 +46,7 @@
 ;; (define-key map [(meta p)]		  'proof-previous-matching-command)
 ;; (define-key map [(meta n)]		  'proof-next-matching-command)
 ;; Standard binding for completion
-(define-key map [(control c) return] 'complete)
+(define-key map [(control return)] 'complete)
 ;(define-key map [(control c) ?u] 'proof-retract-until-point-interactive)
 ;; Add the universal keys bound in all PG buffers.
 (proof-define-keys map proof-universal-keys))
@@ -223,6 +223,7 @@
              :selected proof-electric-terminator-enable]
 	    ["Function menu" function-menu
 	     :active (fboundp 'function-menu)]
+	    ["Complete identifier" complete t]
 	    "----")
           proof-shared-menu)
   "The Proof General generic menu.")