1 files changed, 0 insertions, 60 deletions
diff --git a/coq/todo b/coq/todo
deleted file mode 100644
index eea4427c..00000000
--- a/coq/todo
+++ /dev/null
@@ -1,60 +0,0 @@
--*- mode:outline -*-
-
-* Things to do for Coq
-
-See also ../todo for generic things to do, priority codes.
-
-** A Submit some minor patches to coqdev to improve things:
-      -- no printing of summary proof script, user can see it
-      -- information output when requiring/undoing requires
-      -- more robust markup of errors/responses, eager annotations
-      -- eventually... PGIP
-
-** B Adjust pretty printer line width automatically as others do
-
-** D Coq pbp focussing, would be helpful if this part works at least
-
-** C Auto-compile-vos
-   Would be nice to ressurect this: interaction between PG
-   and make system is tricky and tedious.  
-
-
-** D Loss of synchronisation with silent mode 
-   Apocryphal story, no test cases.
-
-
-** B Proof-by-Pointing [1 month+]  (2002)
-  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.
-  Perhaps for new version of Coq.
-  da: I have old version of code sent to my by Healf.
-  Pierre: Since the code is to be changed, I suggest that we
-  wait for V7.
-  da: V7 is here now...
-
-** C Improve X-Symbol support.  Integrate with Coq syntax mechanism somehow?
-  pierre: Yes, the greatest would be to allow users to easily declare
-  new tokens/symbols and add new grammar rules (Coq allows this)
-  including the declared tokens. Indeed when I define the type set,
-  and its element emptyset, and predicate In, I want to be able to say
-  that emptyset and In are new tokens and asociate them with the right
-  symbols. I want to be able of that on the fly (maybe we can use the
-  'File Variables' feature of Emacs). Another thing is that we may ask
-  Coq developers to be unicode compliant or something like that.
-
-
-** 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)
-  Pierre: I fixed this I think, by making a non-undoable regexp
-  instead. This solves the problem of tactics that have been defined
-  in another file.
-
-** 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]