From f523b125957c2bc7dcbecd08e07ebf9264daa3a5 Mon Sep 17 00:00:00 2001
From: Healfdene Goguen
Date: Thu, 15 Jan 1998 12:13:06 +0000
Subject: One needed change for coq included

---
 todo | 6 ++++++
 1 file changed, 6 insertions(+)

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.
-- 
cgit v1.2.3