diff options
| author |  Matej Kosik <m4tej.kosik@gmail.com> | 2015-11-05 10:43:04 +0100 |
|---|---|---|
| committer |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-12-10 09:35:15 +0100 |
| commit | a90487b5b377c1eadcc4bbb373ad489b4d236a7f (patch) | |
| tree | a48cbc944e253756b885bce693b03f4e51cc79f3 /doc | |
| parent | 02b64e2d6c69996f95fa7bbcaf228e4848ad69f4 (diff) | |
GRAMMAR
Diffstat (limited to 'doc')
| -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 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} |