Remove mmm and ML4PG contribs and remove references to them in code and docs

21 files changed, 1 insertions, 62 deletions

diff --git a/coq/ML4PG/doc/src/images/algorithm1.png b/coq/ML4PG/doc/src/images/algorithm1.png
deleted file mode 100644
index 8c8f47b5..00000000
--- a/coq/ML4PG/doc/src/images/algorithm1.png
+++ /dev/null
diff --git a/coq/ML4PG/doc/src/images/algorithm2.png b/coq/ML4PG/doc/src/images/algorithm2.png
deleted file mode 100644
index 6b5e0835..00000000
--- a/coq/ML4PG/doc/src/images/algorithm2.png
+++ /dev/null
diff --git a/coq/ML4PG/doc/src/images/clusters1.png b/coq/ML4PG/doc/src/images/clusters1.png
deleted file mode 100644
index ca4ef219..00000000
--- a/coq/ML4PG/doc/src/images/clusters1.png
+++ /dev/null
diff --git a/coq/ML4PG/doc/src/images/clusters1pg.png b/coq/ML4PG/doc/src/images/clusters1pg.png
deleted file mode 100644
index b39d409f..00000000
--- a/coq/ML4PG/doc/src/images/clusters1pg.png
+++ /dev/null
diff --git a/coq/ML4PG/doc/src/images/clusters2.png b/coq/ML4PG/doc/src/images/clusters2.png
deleted file mode 100644
index f091abbe..00000000
--- a/coq/ML4PG/doc/src/images/clusters2.png
+++ /dev/null
diff --git a/coq/ML4PG/doc/src/images/clusters2pg.png b/coq/ML4PG/doc/src/images/clusters2pg.png
deleted file mode 100644
index 6ba6dcb4..00000000
--- a/coq/ML4PG/doc/src/images/clusters2pg.png
+++ /dev/null
diff --git a/coq/ML4PG/doc/src/images/export.png b/coq/ML4PG/doc/src/images/export.png
deleted file mode 100644
index de048b47..00000000
--- a/coq/ML4PG/doc/src/images/export.png
+++ /dev/null
diff --git a/coq/ML4PG/doc/src/images/fig1.png b/coq/ML4PG/doc/src/images/fig1.png
deleted file mode 100644
index 955fd048..00000000
--- a/coq/ML4PG/doc/src/images/fig1.png
+++ /dev/null
diff --git a/coq/ML4PG/doc/src/images/fig1pg.png b/coq/ML4PG/doc/src/images/fig1pg.png
deleted file mode 100644
index d4a0df9f..00000000
--- a/coq/ML4PG/doc/src/images/fig1pg.png
+++ /dev/null
diff --git a/coq/ML4PG/doc/src/images/fig2.png b/coq/ML4PG/doc/src/images/fig2.png
deleted file mode 100644
index ed8c399e..00000000
--- a/coq/ML4PG/doc/src/images/fig2.png
+++ /dev/null
diff --git a/coq/ML4PG/doc/src/images/fig3.png b/coq/ML4PG/doc/src/images/fig3.png
deleted file mode 100644
index f3741a0e..00000000
--- a/coq/ML4PG/doc/src/images/fig3.png
+++ /dev/null
diff --git a/coq/ML4PG/doc/src/images/fig4.png b/coq/ML4PG/doc/src/images/fig4.png
deleted file mode 100644
index 9df097bd..00000000
--- a/coq/ML4PG/doc/src/images/fig4.png
+++ /dev/null
diff --git a/coq/ML4PG/doc/src/images/fig5.png b/coq/ML4PG/doc/src/images/fig5.png
deleted file mode 100644
index 733a3d22..00000000
--- a/coq/ML4PG/doc/src/images/fig5.png
+++ /dev/null
diff --git a/coq/ML4PG/doc/src/images/frequencies.png b/coq/ML4PG/doc/src/images/frequencies.png
deleted file mode 100644
index 4f90b5fc..00000000
--- a/coq/ML4PG/doc/src/images/frequencies.png
+++ /dev/null
diff --git a/coq/ML4PG/doc/src/images/granularity.png b/coq/ML4PG/doc/src/images/granularity.png
deleted file mode 100644
index 385b3972..00000000
--- a/coq/ML4PG/doc/src/images/granularity.png
+++ /dev/null
diff --git a/coq/ML4PG/doc/src/images/levels.png b/coq/ML4PG/doc/src/images/levels.png
deleted file mode 100644
index 48e02db7..00000000
--- a/coq/ML4PG/doc/src/images/levels.png
+++ /dev/null
diff --git a/coq/ML4PG/doc/src/images/ml_system1.png b/coq/ML4PG/doc/src/images/ml_system1.png
deleted file mode 100644
index f11cebf1..00000000
--- a/coq/ML4PG/doc/src/images/ml_system1.png
+++ /dev/null
diff --git a/coq/ML4PG/doc/src/images/ml_system2.png b/coq/ML4PG/doc/src/images/ml_system2.png
deleted file mode 100644
index 792c423d..00000000
--- a/coq/ML4PG/doc/src/images/ml_system2.png
+++ /dev/null
diff --git a/coq/coq-abbrev.el b/coq/coq-abbrev.el
index 79231ad9..3a750472 100644
--- a/coq/coq-abbrev.el
+++ b/coq/coq-abbrev.el
@@ -299,10 +299,7 @@ It was constructed with `proof-defstringset-fn'.")
      ["Unset Printing Unfocused" coq-unset-printing-unfocused t]
      ["Set Printing Wildcards" coq-set-printing-wildcards t]
      ["Unset Printing Wildcards" coq-unset-printing-wildcards t]
-     ["Set Printing Width" coq-ask-adapt-printing-width-and-show t])
-    ""
-    ["ML4PG" (coq-activate-ml4pg) :help "Activates ML4PG: machine-learning methods for Proof General"]
-    ))
+     ["Set Printing Width" coq-ask-adapt-printing-width-and-show t])))
 
 (setq-default coq-menu-entries
   (append coq-menu-common-entries
diff --git a/coq/coq-mmm.el b/coq/coq-mmm.el
deleted file mode 100644
index e8ff56eb..00000000
--- a/coq/coq-mmm.el
+++ /dev/null
@@ -1,51 +0,0 @@
-;; coq-mmm.el	  Configure MMM mode for CoqDoc elements
-;;
-;; Copyright     (C) 2007 David Aspinall
-;; Authors:       David Aspinall <David.Aspinall@ed.ac.uk>
-;; Licence:	 GPL
-;;
-;; $Id$
-;;
-;; We only spot some simple cases of embedded LaTeX/HTML/verbatim.
-;;
-;; At the moment, the insertion has a bad interaction with the holes
-;; code which also uses skeletons: the interesting positions used
-;; for MMM markup are made into holes!
-
-(require 'mmm-auto)
-
-(mmm-add-group
- 'coq
- `((coq-text
-   :submode text-mode
-   :face mmm-comment-submode-face
-   :front "(\\*\\*[ \t]"
-   :back  "[ ]?\\*)"
-   :insert ((?d coqdoc-text nil @ "(** " @ " " _ " " @ " *)" @)))
-
-   (coq-latex
-   :submode LaTeX-mode
-   :face mmm-comment-submode-face
-   :front "(\\*\\*[^%\\$]*[%\\$]"
-   :back  "[%\\$][ \t]*\\*)"
-   :insert ((?l coqdoc-latex nil @ "(** %" @ " " _ " " @ "% *)" @)))
-
-   (coq-html
-   :submode html-mode
-   :face mmm-comment-submode-face
-   :front "(\\*\\*[^#]*#"
-   :back  "#[ \t]*\\*)"
-   :insert ((?w coqdoc-html nil @ "(** #" @ " " _ " " @ "# *)" @)))
-
-   (coq-verbatim
-   :submode text-mode
-   :face mmm-code-submode-face
-   :front "^[ \t]*<<"
-   :back  ">>"
-   :insert ((?v coqdoc-verbatim nil @ "<<\n" @ " " _ " " @ "\n>>" @)))
-   ))
-
-
-(provide 'coq-mmm)
-
-;;; coq-mmm.el ends here
diff --git a/coq/coq.el b/coq/coq.el
index 78c48170..d8a52983 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -2844,13 +2844,6 @@ 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
-(declare-function ml4pg-select-mode "ml4pg") ;; Avoids copilation warnings
-
-(defun coq-activate-ml4pg ()
-  (let ((filename (concatenate 'string proof-home-directory "contrib/ML4PG/ml4pg.el")))
-    (when (file-exists-p filename) (load-file filename) (ml4pg-select-mode))))
-
 ;;;;;;;;;;;;;;
 
 ;; This was done in coq-compile-common, but it is actually a good idea even