CLEANUP: the definition of "type of constructor" was rephrased in order to make it more clear

1 files changed, 6 insertions, 3 deletions

diff --git a/doc/refman/RefMan-cic.tex b/doc/refman/RefMan-cic.tex
index 45613e03af..d05e3dd9e8 100644
--- a/doc/refman/RefMan-cic.tex
+++ b/doc/refman/RefMan-cic.tex
@@ -814,9 +814,12 @@ such that $T$ is an arity of sort $s$.
 $A\ra \Set$ and $\forall~A:\Prop,A\ra \Prop$ are arities.
 
 \paragraph[Definition]{Definition\index{type of constructor}}
-A {\em type of constructor of $I$}\index{Type of constructor} is either a term
-$(I~t_1\ldots ~t_n)$ or $\fa x:T,C$ with $C$ recursively 
-a {\em type of constructor of $I$}.
+We say that $T$ is a {\em type of constructor of $I$\index{type of constructor}}
+in one of the following two cases:
+\begin{itemize}
+  \item $T$ is $(I~t_1\ldots ~t_n)$
+  \item $T$ is $\forall x:U,T^\prime$ where $T^\prime$ is also a type of constructor of $I$
+\end{itemize}
 
 \paragraph[Examples]{Examples}
 $\nat$ and $\nat\ra\nat$ are types of constructors of $\nat$.\\