TYPOGRAPHY

1 files changed, 4 insertions, 2 deletions

diff --git a/doc/refman/RefMan-cic.tex b/doc/refman/RefMan-cic.tex
index 8f03cafd14..8f50c1c323 100644
--- a/doc/refman/RefMan-cic.tex
+++ b/doc/refman/RefMan-cic.tex
@@ -771,14 +771,16 @@ rules, we need a few definitions:
 A type $T$ is an {\em arity of sort $s$}\index{Arity} if it converts
 to the sort $s$ or to a product $\forall~x:T,U$ with $U$ an arity
 of sort $s$. (For instance $A\ra \Set$ or $\forall~A:\Prop,A\ra
-\Prop$ are arities of sort respectively \Set\ and \Prop).  A {\em type
+\Prop$ are arities of sort respectively \Set\ and \Prop).
+\vskip.5em
+\noindent 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
 
-The type of constructor $T$ will be said to {\em satisfy the positivity
+\noindent The type of constructor $T$ will be said to {\em satisfy the positivity
 condition} for a constant $X$ in the following cases:
 
 \begin{itemize}