TYPOGRAPHY: 'non dependent product', just like 'dependent product' is now emphasized

1 files changed, 2 insertions, 2 deletions

diff --git a/doc/refman/RefMan-cic.tex b/doc/refman/RefMan-cic.tex
index e33d2259d3..b1becba3f5 100644
--- a/doc/refman/RefMan-cic.tex
+++ b/doc/refman/RefMan-cic.tex
@@ -157,8 +157,8 @@ More precisely the language of the {\em Calculus of Inductive
   occurs in $U$, $\forall~x:T,U$ reads as {\it ``for all x of type T,
     U''}. As $U$ depends on $x$, one says that $\forall~x:T,U$ is a
   {\em dependent product}. If $x$ does not occur in $U$ then
-  $\forall~x:T,U$ reads as {\it ``if T then U''}. A non dependent
-  product can be written: $T \rightarrow U$.
+  $\forall~x:T,U$ reads as {\it ``if T then U''}. A {\em non dependent
+  product} can be written: $T \rightarrow U$.
 \item if $x$ is a variable and $T$, $u$ are terms then $\lb x:T \mto u$
   ($\kw{fun}~x:T~ {\tt =>}~ u$ in \Coq{} concrete syntax) is a term. This is a
   notation for the $\lambda$-abstraction of