diff options
| -rw-r--r-- | doc/refman/RefMan-cic.tex | 2 |
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} |