From a40c4b07059f754e63fa29787148cdab22359cb6 Mon Sep 17 00:00:00 2001
From: Pierre Courtieu
Date: Fri, 16 Apr 2004 12:30:42 +0000
Subject: little fix for x-symbols coq.

---
 CHANGES | 13 +++++++------
 1 file changed, 7 insertions(+), 6 deletions(-)

(limited to 'CHANGES')

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
-- 
cgit v1.2.3