diff options
| -rw-r--r-- | todo | 6 |
1 files changed, 6 insertions, 0 deletions
@@ -49,3 +49,9 @@ o There's a bug so the goal buffer isn't displaying everything that o Sections and files are handled incorrectly. o Update documentation to include C-c C-s. + +o 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 + Lemma y, then finish x, and undo lemma x, then lemma y gets undone + in the buffer as well. |