From ce22b7634aa33afb4f5ee09c2b8c10bf76637234 Mon Sep 17 00:00:00 2001
From: William Lawvere
Date: Sat, 1 Jul 2017 13:47:18 -0700
Subject: RefMan-syn: grammar edit

---
 doc/refman/RefMan-syn.tex | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

(limited to 'doc')

diff --git a/doc/refman/RefMan-syn.tex b/doc/refman/RefMan-syn.tex
index e6eaccb3f8..a409d61bb8 100644
--- a/doc/refman/RefMan-syn.tex
+++ b/doc/refman/RefMan-syn.tex
@@ -701,11 +701,11 @@ Notation}.
 % Introduction
 
 An {\em interpretation scope} is a set of notations for terms with
-their interpretation. Interpretation scopes provides with a weak,
-purely syntactical form of notations overloading: a same notation, for
-instance the infix symbol \verb=+= can be used to denote distinct
-definitions of an additive operator. Depending on which interpretation
-scopes is currently open, the interpretation is different.
+their interpretation. Interpretation scopes provide a weak,
+purely syntactical form of notation overloading: the same notation, for
+instance the infix symbol \verb=+=, can be used to denote distinct
+definitions of the additive operator. Depending on which interpretation
+scope is currently open, the interpretation is different.
 Interpretation scopes can include an interpretation for
 numerals and strings. However, this is only made possible at the
 {\ocaml} level.
-- 
cgit v1.2.3