From f37c09e169b11ed683aeb9147c402b9980a6706c Mon Sep 17 00:00:00 2001
From: Matej Kosik
Date: Mon, 2 Nov 2015 16:28:13 +0100
Subject: TYPOGRAPHY

---
 doc/refman/RefMan-cic.tex | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

(limited to 'doc')

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}
-- 
cgit v1.2.3