Add doc for x-symbols

1 files changed, 26 insertions, 2 deletions

diff --git a/coq/README b/coq/README
index 2689a8d5..4153391e 100644
--- a/coq/README
+++ b/coq/README
@@ -14,11 +14,12 @@ Coq homepage:	http://pauillac.inria.fr/coq/assis-eng.html
 Coq Proof General has experimental multiple file handling for 6.3
 versions.  It does not have support for proof by pointing.
 
-There is support for X Symbol, but not using a proper token language.
+There is support for X Symbol, but using character sequences rather
+than a special token language.  See notes below for syntax.
 
 There is a tags program, coqtags.
 
-========================================
+===========================================================================
 
 Installation notes:
 
@@ -33,6 +34,29 @@ Generate a TAGS file for the library by running
 in the root directory of the library, $COQTOP/theories.  
 
 
+===========================================================================
+
+Grammar for x-symbols:
+
+  Symbols include sequences naming Greek letters ("Lambda", "lambda", etc),
+  connectives /\, \/, etc.  See the X-Symbol char table for details.
+
+  a symbol is encoded only if 
+   - preceded by _ or some space or some symbol
+  **and**
+   - followed by _ or some space or some symbol
+
+  Grammar for sub/superscript: 
+
+   - a double _ introduces a subscript that ends at the first space
+   - a double ^ introduces a superscript that ends at the first space
+  
+   - a _ followed by { introduces a subscript
+     expression that ends at the first }
+   - a ^ followed by { introduces a superscript
+     expression that ends at the first }
+
+
 ========================================
 
 $Id$