One needed change for coq included

1 files changed, 6 insertions, 0 deletions

diff --git a/todo b/todo
index c3c67edc..f4af3662 100644
--- a/todo
+++ b/todo
@@ -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.