aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorHealfdene Goguen1998-05-15 16:28:32 +0000
committerHealfdene Goguen1998-05-15 16:28:32 +0000
commit796d3e6730dc76a21ddf1fe179f8cfc64eecf3c4 (patch)
tree57fa78db0172a6f25cf72e758288e06d5c98a888
parentbc3d75a250e869853b77f4f9da5b62f49dd89332 (diff)
Added problem with indentation.
-rw-r--r--todo8
1 files changed, 8 insertions, 0 deletions
diff --git a/todo b/todo
index 62b5d315..a00c31b0 100644
--- a/todo
+++ b/todo
@@ -28,6 +28,14 @@ A Implement more generic mechanism for large undos (2h)
B Implement proof-find-previous-terminator and bind it to C-c C-a
(45min tms)
+B Find out why a <tab> that doesn't appear to modify the buffer
+ sets the modify flag in the mode-line.
+ (for example, with:
+ Inductive X : Set :=
+ x_i : X.
+ in Coq).
+ (20min hhg)
+
B Technical documentation to record expertise and allow users of other
proof systems to adopt generic package (40h hhg & tms)