fixed some words in coq changes.

1 files changed, 5 insertions, 4 deletions

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