Deleted file

1 files changed, 0 insertions, 92 deletions

diff --git a/coq/TODO-TMP b/coq/TODO-TMP
deleted file mode 100644
index 23b78c02..00000000
--- a/coq/TODO-TMP
+++ /dev/null
@@ -1,92 +0,0 @@
-
-march 6 2008:
--- line ending with *). are swalloawed when queuing.
--- give a cursor back in goal and response buffer!!!
--- have '_' be a symbol constituent AND compatible with font-lock
--- catch window splitting errors when quitting/relaunching coq
-** end march 6 2008
-
-
-
---- multiple file hacking finish
---- X-sym wierdness: (1) (warning/warning) Must provide :input-spec
---- nick ideas from coq-ide: proof wizard
-     (also their goto point is rather nicer: suspect it uses internal 
-	state).
-
---- continue plan of adding more commands to menus, etc
-
---- can we fontify ----- as a rule?
-
---- buggy indentation:
-
-(substring (setq a (shell-command-to-string
-			    (concat
-			     "coqdep *.v | grep " 
-			     (file-name-nondirectory 
-			      (file-name-sans-extension fname)) ".v"
-			      " | awk '{print $1}' | sed 's/.vo:/.v/'")))
-a  -- TAB here loops forever
-
-
-=================================================================
-
-
-;; coq-mmm.el	  Configure MMM mode for Coq (for LaTeX/coqdoc)
-;;
-;; Copyright     (C) 2004 David Aspinall
-;; Authors:       David Aspinall <David.Aspinall@ed.ac.uk>
-;; Licence:	 GPL
-;;
-;; $Id$
-;; 
-;; Presently, we deal with several cases of (** text *).
-;; 
-;; TODO:
-;;  -- complete this
-;;
-
-(require 'mmm-auto)
-
-(defconst coq-start-latex-regexp 
-  (concat
-   "\\(" 
-   (proof-ids-to-regexp 
-    ;; Perhaps section is too much?  The fontification is nice but
-    ;; section headers are a bit short to use LaTeX mode in.
-    (list "text" "header" ".*section"))  
-   ;; Next one is nice but hammers font lock a bit too much
-   ;; if there are lots of -- {* short comments *}
-   ;; "\\|\-\-" ;; NB: doesn't work with \\<--\\>
-   "\\)[ \t]+{\\*"))
-
-(defconst coq-start-sml-regexp 
-  (concat
-   "\\(" 
-   (proof-ids-to-regexp (list "ML" "ML_command" "ML_setup"
-			      "typed_print_translation"))
-   "\\)[ \t]+{\\*"))
-
-
-(mmm-add-group
- 'coq
- `((coq-latex
-   :submode LaTeX-mode
-   :face mmm-comment-submode-face
-   :front ,coq-start-latex-regexp 
-   :back  "\\*}"
-   :insert ((?t coqtext nil @ "text {*" @ " " _ " " @ "*}" @))
-   :save-matches 1)
-
-  (coq-sml
-   :submode sml-mode
-   :face mmm-code-submode-face
-   :front ,coq-start-sml-regexp
-   :back  "\\*}"
-   :insert ((?M coqml nil @ "ML_setup {*" @ " " _ " " @ "*}" @))
-   :save-matches 1)))
-   
-
-(provide 'coq-mmm)
-
-;;; coq-mmm.el ends here