diff options
| author |  charguer <arthur@chargueraud.org> | 2018-03-08 12:15:41 +0100 |
|---|---|---|
| committer |  Maxime Dénès <mail@maximedenes.fr> | 2018-03-09 13:31:51 +0100 |
| commit | 056c2cf46acfc1edcecf8e9b6f969b0415f78b52 (patch) | |
| tree | c74e8eb3d9bf08a0099eb91cda60fa4ae47bdca0 /doc | |
| parent | 1274261b6ac020468ac6f24d68de723ae1259c42 (diff) | |
doc and changes for coercion from prop/type
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/refman/Coercion.tex | 7 |
1 files changed, 3 insertions, 4 deletions
diff --git a/doc/refman/Coercion.tex b/doc/refman/Coercion.tex index ec46e1eb5..53b6b7827 100644 --- a/doc/refman/Coercion.tex +++ b/doc/refman/Coercion.tex @@ -33,7 +33,7 @@ classes: \begin{itemize} \item {\tt Sortclass}, the class of sorts; - its objects are the terms whose type is a sort. + its objects are the terms whose type is a sort (e.g., \ssrC{Prop} or \ssrC{Type}). \item {\tt Funclass}, the class of functions; its objects are all the terms with a functional type, i.e. of form $forall~ x:A, B$. @@ -73,8 +73,8 @@ conditions holds: We then write $f:C \mbox{\texttt{>->}} D$. The restriction on the type of coercions is called {\em the uniform inheritance condition}. -Remark that the abstract classes {\tt Funclass} and {\tt Sortclass} -cannot be source classes. +Remark: the abstract class {\tt Sortclass} can be used as source class, +but the abstract class {\tt Funclass} cannot. To coerce an object $t:C~t_1..t_n$ of $C$ towards $D$, we have to apply the coercion $f$ to it; the obtained term $f~t_1..t_n~t$ is @@ -160,7 +160,6 @@ Declares the construction denoted by {\qualid} as a coercion between \item {\qualid} \errindex{not declared} \item {\qualid} \errindex{is already a coercion} \item \errindex{Funclass cannot be a source class} -\item \errindex{Sortclass cannot be a source class} \item {\qualid} \errindex{is not a function} \item \errindex{Cannot find the source class of {\qualid}} \item \errindex{Cannot recognize {\class$_1$} as a source class of {\qualid}} |