-*- mode:outline -*-

* Things to do for Coq

See also ../todo for generic things to do, priority codes.


** B See if there is a way to turn off the superfluous output of scripts

  from Coq when inside ProofGeneral, i.e. output like this:

   Intros A B G.
   Induction G.
   Apply conj.
   Assumption.
   
   Assumption.
   
   and_comms is defined

  In PG, only the last line is relevant!!
  If it isn't possible to turn it off, can we send a suggestion
  to the Coq implementors for the next version?

** B Fix silly startup sychronization problem that displays
  cwd on startup.

** 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 [2 weeks]
  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.

** 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)

** C Correct the C-c C-c bug (typing C-c C-c during the execution of a
   tactic breaks the consitency with Coq)

** C Fix the coq-lift-global code

** 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]