From 229b06e7b4b4addeec4323c1243270c510733a9f Mon Sep 17 00:00:00 2001 From: Pierre Courtieu Date: Thu, 15 Apr 2004 08:01:16 +0000 Subject: fixed some words in coq changes. --- CHANGES | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) (limited to 'CHANGES') diff --git a/CHANGES b/CHANGES index c78747a3..eb6d042e 100644 --- a/CHANGES +++ b/CHANGES @@ -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 -- cgit v1.2.3