diff options
| -rw-r--r-- | doc/refman/RefMan-cic.tex | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/doc/refman/RefMan-cic.tex b/doc/refman/RefMan-cic.tex index 4d473d54b6..9660a04bd5 100644 --- a/doc/refman/RefMan-cic.tex +++ b/doc/refman/RefMan-cic.tex @@ -1225,8 +1225,8 @@ $I$. \begin{description} \item[Prod] \inference{\frac{\compat{(I~x):A'}{B'}} - {\compat{I:(x:A)A'}{(x:A)B'}}} -\item[\Set \& \Type] \inference{\frac{ + {\compat{I:\forall x:A, A'}{\forall x:A, B'}}} +\item[{\Set} \& \Type] \inference{\frac{ s_1 \in \{\Set,\Type(j)\}, s_2 \in \Sort}{\compat{I:s_1}{I\ra s_2}}} \end{description} |