aboutsummaryrefslogtreecommitdiffhomepage
path: root/COMPATIBILITY
diff options
context:
space:
mode:
authorGravatar David Aspinall <da@inf.ed.ac.uk>2007-12-12 20:22:17 +0000
committerGravatar David Aspinall <da@inf.ed.ac.uk>2007-12-12 20:22:17 +0000
commit7a92ceb76543508bcdadaa9b625f851ea8900c5c (patch)
tree433809631855fda09694debae91002f5ee2d5085 /COMPATIBILITY
parent1baea2b15bfdefacdbeccc1a626f5402b4ace99c (diff)
Updated.
Diffstat (limited to 'COMPATIBILITY')
-rw-r--r--COMPATIBILITY19
1 files changed, 12 insertions, 7 deletions
diff --git a/COMPATIBILITY b/COMPATIBILITY
index c590d705..83ab1e99 100644
--- a/COMPATIBILITY
+++ b/COMPATIBILITY
@@ -1,3 +1,6 @@
+Compatibility of Proof General
+==============================
+
This version of Proof General has been tested with these Emacs versions
on Linux:
@@ -11,15 +14,17 @@ and prover versions:
Isabelle2005
Isabelle2007
-For more possibilities, please check and contribute here:
-
- http://proofgeneral.inf.ed.ac.uk/wiki/Main/PGEmacsVer37Final
+Maintaining compatibility across proof assistant versions, Emacs
+versions and operating systems is a big challenge! Please visit this
+wiki page to check on others experience and report your own:
------
+ http://proofgeneral.inf.ed.ac.uk/wiki/Main/PGEmacsCompatibility
-Backward compatibility makes the code into a bad mess. Some compatibility
-has been removed here, specifically affecting:
- Isabelle 2004
+Backward compatibility and version-specific Emacs patches makes the
+code into a bad mess. Some compatibility has been removed here,
+specifically affecting:
+ Coq 7
+ Isabelle 2004
Earlier buggy versions of Emacs 21 (21.4.1 should work)