aboutsummaryrefslogtreecommitdiffhomepage
path: root/CHANGES
diff options
context:
space:
mode:
authorGravatar Pierre Courtieu <courtieu@lri.fr>2004-04-16 12:30:42 +0000
committerGravatar Pierre Courtieu <courtieu@lri.fr>2004-04-16 12:30:42 +0000
commita40c4b07059f754e63fa29787148cdab22359cb6 (patch)
treee55100008e2a9615910648cede16436d21e36f7c /CHANGES
parent665fcf2a7667f428ca0be6fc31ba14117ab11c68 (diff)
little fix for x-symbols coq.
Diffstat (limited to 'CHANGES')
-rw-r--r--CHANGES13
1 files changed, 7 insertions, 6 deletions
diff --git a/CHANGES b/CHANGES
index f9bf3b14..b95054bb 100644
--- a/CHANGES
+++ b/CHANGES
@@ -259,12 +259,13 @@ will be asked if you want to save abbrevs, answer yes.
*** X-symbols are much improved (more symbols, cleaner grammar)
-Symbols are encoded only if between spaces or _'s. Sub/superscripts
-are now introduced by '__' and '^^' respectively, and the rest of the
-word is sub/superscripted. To put spaces inside sub/superscripts, use
-_{...} or ^{...}. Notice that this last syntax is not understood by
-Coq and you will need to defined it with the "Notation" command of
-Coq.
+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.
** Additional instances of Proof General