GRAMMAR

1 files changed, 1 insertions, 1 deletions

diff --git a/doc/refman/RefMan-cic.tex b/doc/refman/RefMan-cic.tex
index 7c38a54ea..611782b4f 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}