aboutsummaryrefslogtreecommitdiffhomepage
path: root/coq
diff options
context:
space:
mode:
authorGravatar David Aspinall <da@inf.ed.ac.uk>2004-04-23 10:28:15 +0000
committerGravatar David Aspinall <da@inf.ed.ac.uk>2004-04-23 10:28:15 +0000
commit21371a3d0691999b8ffb131cb1541a608b628dd7 (patch)
tree819c078c2f8870d4e73fddb832bcb428aaa33518 /coq
parent49e4b9daffaf2edbbe318d8bc5f102e036cd9724 (diff)
Updated.
Diffstat (limited to 'coq')
-rw-r--r--coq/todo7
1 files changed, 7 insertions, 0 deletions
diff --git a/coq/todo b/coq/todo
index 5507ba79..eea4427c 100644
--- a/coq/todo
+++ b/coq/todo
@@ -4,6 +4,13 @@
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