aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--CHANGES8
-rw-r--r--coq/README14
2 files changed, 9 insertions, 13 deletions
diff --git a/CHANGES b/CHANGES
index 41c46807..fc9a86ef 100644
--- a/CHANGES
+++ b/CHANGES
@@ -261,13 +261,7 @@ will be asked if you want to save abbrevs, answer yes.
*** X-symbols are much improved (more symbols, cleaner grammar)
Much more symbols are supported now (C-= C-= for the symbol table).
-Symbols are encoded only if between spaces, ' or _. Sub/superscripts
-are now introduced by '__' and '^^' respectively, and then the word is
-sub/superscripted until its end. To put spaces or symbols inside
-sub/superscripts, use _{...} or ^{...}. Notice that this last syntax
-and the ^^ symbol are not understood by Coq and you will need to
-defined it with the "Notation" command of Coq.
-
+See coq/README for the syntax of sub/superscripts.
** Additional instances of Proof General
diff --git a/coq/README b/coq/README
index 97ea8ec8..dc0bd3bc 100644
--- a/coq/README
+++ b/coq/README
@@ -46,20 +46,22 @@ Grammar for x-symbols:
connectives /\, \/, etc. See the X-Symbol char table for details.
a symbol is encoded only if
- - preceded by _ or some space or some symbol
+ - preceded by _ or ' or some space or some symbol
**and**
- - followed by _ or some space or some symbol
+ - followed by _ or ' 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 }
+ - a , followed by { introduces a subscript expression that ends at
+ the first } (_{...} was not possible due to coq notation mechanism)
+ - a ^ followed by { introduces a superscript expression that ends
+ at the first }
+
+ See example-x-symbols.v in this directory for examples.
========================================