diff options
| -rw-r--r-- | etc/README | 10 | ||||
| -rw-r--r-- | etc/bug-notes.txt | 16 |
2 files changed, 6 insertions, 20 deletions
@@ -14,10 +14,12 @@ ProofGeneral.desktop Menu file for some Linux versions. announce Announcement -lego Files for testing LEGO Proof General -isa Isabelle Proof General -isar Isar PG -demoisa Isabelle Demo PG +lego Files for testing: LEGO Proof General +isa Isabelle Proof General +isar Isar PG +demoisa Isabelle Demo PG +coq Coq +<otherprover> .. others, similarly bug-notes.txt Test cases for Emacs or PG bugs diff --git a/etc/bug-notes.txt b/etc/bug-notes.txt index c4aaf21d..e00a23e7 100644 --- a/etc/bug-notes.txt +++ b/etc/bug-notes.txt @@ -6,22 +6,6 @@ Test cases for PG and/or Emacs bugs. ---------------- -* Coq, and others bug: synchronization not gained until second line. - -Test in Coq buffer: - - Print foo. - -Should give error, but PG ignores it and colours command blue. -Similar errors for some other provers. - -[ Now fixed in 3.2pre ] - - - - ----------------- - * XEmacs bug: buffer-syntactic-context-depth returns weird values Seems to depend on previous history. Test in Coq buffer: |