TYPOGRAPHY: Examples of "arity" concept(s) were put to a separate \paragraph{...}

1 files changed, 15 insertions, 8 deletions

diff --git a/doc/refman/RefMan-cic.tex b/doc/refman/RefMan-cic.tex
index deaa1047c8..2fa9c59a86 100644
--- a/doc/refman/RefMan-cic.tex
+++ b/doc/refman/RefMan-cic.tex
@@ -766,16 +766,23 @@ We restrict ourselves to definitions which
 satisfy a syntactic criterion of positivity. Before giving the formal
 rules, we need a few definitions:
 
-\paragraph[Definitions]{Definitions\index{Positivity}\label{Positivity}}
-
-A type $T$ is an {\em arity of sort $s$}\index{Arity} if it converts
+\paragraph[Definition]{Definition\index{Arity}\label{Arity}}
+A type $T$ is an {\em arity of sort $s$} 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).
-\vskip.5em
-\noindent A type $T$ is an {\em arity} if there is a $s\in\Sort$
+of sort $s$.
+
+\paragraph[Examples]{Examples}
+$A\ra \Set$ is an arity of sort $\Set$.
+$\forall~A:\Prop,A\ra \Prop$ is an arity of sort \Prop.
+
+\paragraph[Definition]{Definition}
+A type $T$ is an {\em arity} if there is a $s\in\Sort$
 such that $T$ is an arity of sort $s$.
-\vskip.5em
+
+\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
 $(I~t_1\ldots ~t_n)$ or $\fa x:T,C$ with $C$ recursively