From e560bee8dedb971ee132742109ac27ecddb55975 Mon Sep 17 00:00:00 2001
From: Ricky Elrod
Date: Sun, 15 May 2016 01:19:53 -0400
Subject: Fix a really small doc typo

---
 doc/refman/RefMan-syn.tex | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/doc/refman/RefMan-syn.tex b/doc/refman/RefMan-syn.tex
index 3af72db78e..1f08b6a2f1 100644
--- a/doc/refman/RefMan-syn.tex
+++ b/doc/refman/RefMan-syn.tex
@@ -358,7 +358,7 @@ state of {\Coq}.
 Reserved Notation "x = y" (at level 70, no associativity).
 \end{coq_example}
 
-Reserving a notation is also useful for simultaneously defined an
+Reserving a notation is also useful for simultaneously defining an
 inductive type or a recursive constant and a notation for it.
 
 \Rem The notations mentioned on Figure~\ref{init-notations} are
-- 
cgit v1.2.3