Split low-level todo into several files.

1 files changed, 36 insertions, 0 deletions

diff --git a/coq/todo b/coq/todo
new file mode 100644
index 00000000..827df50f
--- /dev/null
+++ b/coq/todo
@@ -0,0 +1,36 @@
+-*- mode:outline -*-
+
+* See also ../todo for generic things to do, priority codes.
+
+* Things to do for Coq
+======================
+
+B C-c C-c breaks the coherence with prover state
+  (da: can somebody tell me if this is still true? 
+   what problem specifically?)
+
+B Proof-by-Pointing [1 month]
+  da: Yves Bertot told me that his CtCoq proof-by-pointing code
+  is in the Coq kernel now, so would be useful for PG.
+  We need a Coq hacker to do this (Pierre?)
+
+C Improve X-Symbol support.  Integrate with Coq syntax mechanism somehow?
+
+C Retraction in a Section should retract to the beginning of the whole 
+  section. See the section "Granularity of
+  Atomic Commands" for a proposal on how to generalise the current
+  implementation so that it can also deal with sections.
+  [See also the LEGO problem with Discharge] (6h)
+
+D Add Patrick Loiseleur's commands to search for vernac or ml files.
+  (they are in a separate file that is part of Coq distrib.
+   should I really integrate that in PG ? Patrick) 
+  (maybe not if they're orthogonal to PG, but might help users - da)
+
+D Add coq-add-tactic with a tactic name, which adds that tactic to the 
+  undoable tactics and to the font-lock. (2h)
+
+D Improve coqtags. It cannot handle lists e.g., with 	
+	Parameter x,y:nat
+  it only tags x but not y. [The same problem exists for legotags]
+