GRAMMAR

1 files changed, 1 insertions, 1 deletions

diff --git a/doc/refman/RefMan-cic.tex b/doc/refman/RefMan-cic.tex
index a5832450ce..14a5e12fc5 100644
--- a/doc/refman/RefMan-cic.tex
+++ b/doc/refman/RefMan-cic.tex
@@ -1160,7 +1160,7 @@ hence, if \texttt{option} is applied to a type in {\Set}, the result is
 in {\Set}. Note that if \texttt{option} is applied to a type in {\Prop},
 then, the result is not set in \texttt{Prop} but in \texttt{Set}
 still. This is because \texttt{option} is not a singleton type (see
-section~\ref{singleton}) and it would loose the elimination to {\Set} and
+section~\ref{singleton}) and it would lose the elimination to {\Set} and
 {\Type} if set in {\Prop}.
 
 \begin{coq_example}