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
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
|
-*- 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?)
Pierre: I never had this problem, it's all I can say
** 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.
Pierre: Since the code is to be changed, I suggest that we
wait for V7.
** 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.
** 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)
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]
|
