diff options
-rw-r--r-- | CHANGES | 9 |
1 files changed, 5 insertions, 4 deletions
@@ -214,16 +214,17 @@ Holes are a powerful feature for complex expression editing. It is inspired from other tools, like Pcoq (http://www-sop.inria.fr/lemme/pcoq/index.html). The principle is simple, holes are pieces of text that can be "filled" by different -means. The new menu system makes use of the hole system. Almost all -holes operation are available in the Coq/holes menu. +means. The new menu system makes use of the holes system. Almost all +holes operations are available in the Coq/holes menu. *** 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 syntax is not understood by Coq -and you will need to defined it with the "Notation" command of Coq. +_{...} or ^{...}. Notice that this last syntax is not understood by +Coq and you will need to defined it with the "Notation" command of +Coq. ** Additional instances of Proof General |