Update for Unicode Tokens.

1 files changed, 9 insertions, 4 deletions

diff --git a/coq/README b/coq/README
index 746d34d1..dbb77ba8 100644
--- a/coq/README
+++ b/coq/README
@@ -11,7 +11,7 @@ Coq homepage:	http://coq.inria.fr/
 
 ===========================================================================
 
-Coq Proof General has support for X Symbol, using simple character
+Coq Proof General has support for Unicode Tokens, using simple character
 sequences rather than a special language of tokens (which works well
 with V8's new syntax!).  See notes below.
 
@@ -31,16 +31,21 @@ Install coqtags in a standard place or add <proof-home>/coq to your PATH.
 NB: You may need to change the path to perl at the top of the file.
 
 Generate a TAGS file for the library by running
+
 	coqtags `find . -name \*.v -print`
+
 in the root directory of the library, $COQTOP/theories.  
 
 
 ===========================================================================
 
-Grammar for x-symbols:
+Grammar for Unicode Tokens:
 
   Symbols include sequences naming Greek letters ("Lambda", "lambda", etc),
-  connectives /\, \/, etc.  See the X-Symbol char table for details.
+  connectives /\, \/, etc.  See the token list (Unicode Tokens -> List Tokens)
+  for tokens availabe --- these are just a sample set and you can add your own.
+
+  See coq-unicode-tokens.el for the tables and further instructions.
 
   a symbol is encoded only if 
    - preceded by _ or ' or some space or some symbol
@@ -58,7 +63,7 @@ Grammar for x-symbols:
    - a ^ followed by { introduces a superscript expression that ends
      at the first }
 
-	See example-x-symbols.v in this directory for examples.
+	See example-tokens.v in this directory for examples.
 
 ========================================