aboutsummaryrefslogtreecommitdiffhomepage
path: root/coq/TODO-TMP
blob: 25a227b275918286041ff88bc9490c4391cf2b58 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
--- 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