From 2783aa1f5955cd865029c3f685a44d42e39c7e51 Mon Sep 17 00:00:00 2001
From: Dilip Sequiera
Date: Mon, 17 Nov 1997 17:11:23 +0000
Subject: Added some magic commands: proof-frob-locked-end, proof-try-command,
 proof-interrupt-process. Added moving nested lemmas above goal for coq.
 Changed the key mapping for assert-until-point to C-c RET.

---
 todo | 27 +++++++++++++++++++++++++++
 1 file changed, 27 insertions(+)
 create mode 100644 todo

(limited to 'todo')

diff --git a/todo b/todo
new file mode 100644
index 00000000..4d1a73b1
--- /dev/null
+++ b/todo
@@ -0,0 +1,27 @@
+This is a list of things which need doing to the lego mode.
+
+* Fixing up errors caused by pbp-generated commands.
+
+* undo support for LEGO needs to consider Discharge; perhaps unrol to
+  the beginning of the module?
+
+* pbp code doesn't quite accord with the tech report; in particular it
+  decodes annotations eagerly. Lazily would be faster, and it's what
+  the tech report claims
+
+* It would be nice to have a version ported to emacs19 (or
+  20). Unfortunately, it's currently impossible to port the pbp code,
+  since emacs19 doesn't properly handle highlighting of nested
+  overlays. The bulk of the stuff dependent on which version of emacs
+  is running has been moved to proof-dependencies.el, but there are
+  doubtless differences in font-locking and menu code which will
+  require some work.
+
+* Indentation - LEGO should indent only with brackets; Coq for Inductive
+  definitions and 'case' constructs also.
+
+* file handling could be more robust
+
+* For Coq:
+   Fill in proof-shell-interrupt-regexp
+   Fill in proof-state-preserving-p
-- 
cgit v1.2.3