From 6a54c04d60038fbf5b617ee76bb59216ff4038d4 Mon Sep 17 00:00:00 2001
From: Matej Kosik
Date: Thu, 5 Nov 2015 17:20:23 +0100
Subject: GRAMMAR

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

diff --git a/doc/refman/RefMan-cic.tex b/doc/refman/RefMan-cic.tex
index 7c38a54ea6..611782b4f6 100644
--- a/doc/refman/RefMan-cic.tex
+++ b/doc/refman/RefMan-cic.tex
@@ -1450,7 +1450,7 @@ a logical property of a computational object.
 In the same spirit, elimination on $P$ of type $I\ra
 \Type$ cannot be allowed because it trivially implies the elimination
 on $P$ of type $I\ra \Set$ by cumulativity. It also implies that there
-is two proofs of the same property which are provably different,
+are two proofs of the same property which are provably different,
 contradicting the proof-irrelevance property which is sometimes a
 useful axiom:
 \begin{coq_example}
-- 
cgit v1.2.3