diff options
| author |  joheras <> | 2013-05-30 13:18:23 +0000 |
|---|---|---|
| committer | joheras <> | 2013-05-30 13:18:23 +0000 |
| commit | 884f571b13a8279a1169d9f4acd7696b8cb8200b (patch) | |
| tree | cf71e27b09a56137c1ac03737c9955457d78f857 | |
| parent | 764a7f8e44f7412de80a4feb350aaa9bdd060b44 (diff) | |
ML4PG functionality added to Coq menu
| -rw-r--r-- | coq/coq-abbrev.el | 5 | ||||
| -rw-r--r-- | coq/coq.el | 8 |
2 files changed, 12 insertions, 1 deletions
diff --git a/coq/coq-abbrev.el b/coq/coq-abbrev.el index 8f5f6634..b060a101 100644 --- a/coq/coq-abbrev.el +++ b/coq/coq-abbrev.el @@ -174,7 +174,10 @@ ["Set Printing Coercions" coq-set-printing-coercions t] ["Unset Printing Coercions" coq-unset-printing-coercions t] ["Set Printing Wildcards" coq-set-printing-wildcards t] - ["Unset Printing Wildcards" coq-unset-printing-wildcards t]))) + ["Unset Printing Wildcards" coq-unset-printing-wildcards t]) + "" + ["ML4PG" (coq-activate-ml4pg) :help "Activates ML4PG: machine-learning methods for Proof General"] + )) (defpgdefault menu-entries (append coq-menu-common-entries @@ -2080,6 +2080,14 @@ are non-nil at the same time, this gives priority to the former." ;(define-key coq-mode-map (kbd ".") 'coq-terminator-insert) ;(define-key coq-mode-map (kbd ";") 'coq-terminator-insert) ; for french keyboards +;; Activation of ML4PG functionality + +(defun coq-activate-ml4pg () + (load-file (concatenate 'string proof-home-directory "coq/ML4PG/ml4pg.el")) + (ml4pg-select-mode)) + + + (provide 'coq) |