aboutsummaryrefslogtreecommitdiffhomepage
path: root/coq/README
diff options
context:
space:
mode:
authorGravatar David Aspinall <da@inf.ed.ac.uk>2004-04-21 22:21:28 +0000
committerGravatar David Aspinall <da@inf.ed.ac.uk>2004-04-21 22:21:28 +0000
commit0baa4761f4482643c2368365ea679663313ae59e (patch)
tree0e745c90496b743d8a2ecf8552be679448fa56d3 /coq/README
parenteae3591e862d9399d3040cbebbc78f8bbbb2f3ca (diff)
Updated.
Diffstat (limited to 'coq/README')
-rw-r--r--coq/README9
1 files changed, 6 insertions, 3 deletions
diff --git a/coq/README b/coq/README
index 4153391e..bc36df84 100644
--- a/coq/README
+++ b/coq/README
@@ -11,14 +11,17 @@ Coq homepage: http://pauillac.inria.fr/coq/assis-eng.html
===========================================================================
-Coq Proof General has experimental multiple file handling for 6.3
+Coq Proof General has experimental multiple file handling for some
versions. It does not have support for proof by pointing.
-There is support for X Symbol, but using character sequences rather
-than a special token language. See notes below for syntax.
+There is support for X Symbol, using simple character sequences rather
+than a special language of tokens. See notes below for syntax.
There is a tags program, coqtags.
+There is a menu option for running Coq V8 in compatibility mode
+(i.e. with the -translate flag).
+
===========================================================================
Installation notes: