From 0baa4761f4482643c2368365ea679663313ae59e Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Wed, 21 Apr 2004 22:21:28 +0000 Subject: Updated. --- coq/README | 9 ++++++--- 1 file changed, 6 insertions(+), 3 deletions(-) (limited to 'coq/README') 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: -- cgit v1.2.3