diff options
author | David Aspinall <da@inf.ed.ac.uk> | 2007-12-13 12:58:11 +0000 |
---|---|---|
committer | David Aspinall <da@inf.ed.ac.uk> | 2007-12-13 12:58:11 +0000 |
commit | d64389d34f3494b97c67b7a6094123f1a699040c (patch) | |
tree | 67c8fd95283d89a960240200970a9a2b134cb67b /lego | |
parent | 44d5bf78ff00eb2d48f111d8d8718aa3b8ad010c (diff) |
Deleted file
Diffstat (limited to 'lego')
-rw-r--r-- | lego/todo | 44 |
1 files changed, 0 insertions, 44 deletions
diff --git a/lego/todo b/lego/todo deleted file mode 100644 index dc0b1f28..00000000 --- a/lego/todo +++ /dev/null @@ -1,44 +0,0 @@ --*- mode:outline -*- - -* Things to do for LEGO - -See also ../todo for generic things to do, priority codes. - -** C Improve X-Symbol support. - -** D Fix Pbp implementation in LEGO itself (10h) - -** D In LEGO, apart from Goal...Save pairs, we have - declaration...discharge pairs. See the section "Granularity of - Atomic Commands" for a proposal on how to generalise the current - implementation so that it can also deal with "Discharge". - [See also the Coq problem with Sections] (6h) - -** D Inoking an "Expand" command produces a new proof state. But this is - incorrectly displayed in the response buffer and not the goals - buffer because special annotations are missing. Presumably, one - ought to replace "Toplevel.Pr()" by "Toplevel.PR()" in the - definition of "Expand" (see file newtop.sml [Version 1.4]). (30min) - -** D Even with the more flexible region model, with - proof-nested-goals-behaviour=closequick, Proof General doesn't - do quite the right thing. Forget for a definition when inside - a proofstate kills off the whole proofstate. Effectively, - the definition is *global* rather than local to the proofstate, - and could perhaps be lifted to before the goal - (with the lift-global nonsense not so daft after all? Editing - behind the user's back is still objectionable though). - Another alternative fix would be to trigger some retraction action - on seeing the "Abort" regexp, rather than assuming it is the result of - some retraction action. More generally this could be used for error - handling. - -** D Improve legotags. It cannot handle lists e.g., with - [x,y:nat]; - it only tags x but not y. [The same problem exists for coqtags] - -** X Mechanism to save object file. Specifically, after having processed - a script (interactively), it would be nice if one could now save the - buffer in object format. At the moment, it only gets converted - (automatically) when it is read in indirectly at a later stage. - However, there is currently no LEGO command to do this. [4h] |