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