From 884f571b13a8279a1169d9f4acd7696b8cb8200b Mon Sep 17 00:00:00 2001
From: joheras
Date: Thu, 30 May 2013 13:18:23 +0000
Subject: ML4PG functionality added to Coq menu

---
 coq/coq-abbrev.el | 5 ++++-
 coq/coq.el        | 8 ++++++++
 2 files changed, 12 insertions(+), 1 deletion(-)

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
diff --git a/coq/coq.el b/coq/coq.el
index 77af9b9e..69bdce06 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -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)
 
-- 
cgit v1.2.3