diff options
| author |  Healfdene Goguen <da+pg-hhg@inf.ed.ac.uk> | 1998-05-05 14:29:39 +0000 |
|---|---|---|
| committer | Healfdene Goguen <da+pg-hhg@inf.ed.ac.uk> | 1998-05-05 14:29:39 +0000 |
| commit | 3f95f37c64e21134aa909f7adaf3a8141fe12fd8 (patch) | |
| tree | bb7519e2e7fc641deac352bdfaddf7bcbe50a0c2 | |
| parent | 4fd46892ed94591610ef4027aaa4a8f7d24fb271 (diff) | |
Coq now restarts if going back to beginning of proof.
| -rw-r--r-- | todo | 4 |
1 files changed, 1 insertions, 3 deletions
@@ -88,15 +88,13 @@ A Error messages need to be revised e.g., if an import fails, LEGO * Here are things to be done to Coq mode ======================================== -A Restart if going back to beginning of proof. (30min hhg) - ? There's a bug so the goal buffer isn't displaying everything that happens. C Sections and files are handled incorrectly. A Update documentation to include C-c C-s. (10min hhg) - + A Lifted nested lemmas respond incorrectly to C-c u: Coq gets sent the correct command if I undo up to the lower lemma, but the buffer undoes to the upper lemma. I.e., if I start Lemma x, then prove |