diff options
author | Pierre Courtieu <courtieu@lri.fr> | 2004-04-16 12:30:42 +0000 |
---|---|---|
committer | Pierre Courtieu <courtieu@lri.fr> | 2004-04-16 12:30:42 +0000 |
commit | a40c4b07059f754e63fa29787148cdab22359cb6 (patch) | |
tree | e55100008e2a9615910648cede16436d21e36f7c /CHANGES | |
parent | 665fcf2a7667f428ca0be6fc31ba14117ab11c68 (diff) |
little fix for x-symbols coq.
Diffstat (limited to 'CHANGES')
-rw-r--r-- | CHANGES | 13 |
1 files changed, 7 insertions, 6 deletions
@@ -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 |