blob: 8cbac6f5b8c103a73fd28dd50aad03be46b2d714 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
|
-*- 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]
|
