aboutsummaryrefslogtreecommitdiffhomepage
path: root/CHANGES
diff options
context:
space:
mode:
authorGravatar David Aspinall <da@inf.ed.ac.uk>2003-03-03 21:47:02 +0000
committerGravatar David Aspinall <da@inf.ed.ac.uk>2003-03-03 21:47:02 +0000
commitdcfc03d0fc742613700ca4106d14a95fe22c31bb (patch)
treedd2fcd02c58d47d2aca3bdcc4af31632d18da22c /CHANGES
parentdc9cb71adade623abd8093a65f363e6c6552c3e0 (diff)
Remove newlines patch for Coq
Diffstat (limited to 'CHANGES')
-rw-r--r--CHANGES10
1 files changed, 1 insertions, 9 deletions
diff --git a/CHANGES b/CHANGES
index c20d4af0..e185cd53 100644
--- a/CHANGES
+++ b/CHANGES
@@ -14,7 +14,7 @@
Proof General can now (almost) be reliably run as compiled code.
- *** Please help me iron out any finaly difficulties
+ *** Please help me iron out any final difficulties
by reporting problems ***
However, compiled Emacs Lisp files sometimes have incompatibilities
@@ -79,14 +79,6 @@ NB: Not yet enabled for Isabelle/Isar.
Electric terminator menu option more visible.
Reduce contrast for mouse highlighting of regions.
-*** Support formatted input which contains newlines [for Coq]
-
-A patch from Stefan Monnier, to allow Coq input to have newlines
-remaining, so that input formatting is not broken. A much better way
-to address this would be to alter the Coq output routines so that they
-do not print multiple identical prompts for continued lines.
-[this is in testing: please notify me of problems in other provers]
-
** GNU Emacs compatibility, simplified font-lock, handling nested comments