ENH: examples

1 files changed, 7 insertions, 5 deletions

diff --git a/doc/refman/RefMan-cic.tex b/doc/refman/RefMan-cic.tex
index 2fa9c59a86..d0bffa06e7 100644
--- a/doc/refman/RefMan-cic.tex
+++ b/doc/refman/RefMan-cic.tex
@@ -782,15 +782,17 @@ such that $T$ is an arity of sort $s$.
 \paragraph[Examples]{Examples}
 $A\ra \Set$ and $\forall~A:\Prop,A\ra \Prop$ are arities.
 
-\paragraph[Definition]{Definition\index{Positivity}\label{Positivity}}
-\noindent A {\em type
-  of constructor of $I$}\index{Type of constructor} is either a term
+\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$}.
 
-\smallskip
+\paragraph[Examples]{Examples}
+$\nat$ and $\nat\ra\nat$ are types of constructors of $\nat$.\\
+$\forall A:\Type,\List~A$ and $\forall A:\Type,A\ra\List~A\ra\List~A$ are constructors of $\List$.
 
-\noindent The type of constructor $T$ will be said to {\em satisfy the positivity
+\paragraph[Definition]{Definition\index{Positivity}\label{Positivity}}
+The type of constructor $T$ will be said to {\em satisfy the positivity
 condition} for a constant $X$ in the following cases:
 
 \begin{itemize}