From a90487b5b377c1eadcc4bbb373ad489b4d236a7f Mon Sep 17 00:00:00 2001 From: Matej Kosik Date: Thu, 5 Nov 2015 10:43:04 +0100 Subject: GRAMMAR --- doc/refman/RefMan-cic.tex | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'doc') diff --git a/doc/refman/RefMan-cic.tex b/doc/refman/RefMan-cic.tex index a5832450c..14a5e12fc 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} -- cgit v1.2.3