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

2 files changed, 4 insertions, 4 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
diff --git a/doc/refman/RefMan-gal.tex b/doc/refman/RefMan-gal.tex
index f631c3717c..0e758bcab6 100644
--- a/doc/refman/RefMan-gal.tex
+++ b/doc/refman/RefMan-gal.tex
@@ -468,8 +468,8 @@ proposition $B$ or the functional dependent product from $A$ to $B$ (a
 construction usually written $\Pi_{x:A}.B$ in set theory).
 
 Non dependent product types have a special notation: ``$A$ {\tt ->}
-$B$'' stands for ``{\tt forall \_:}$A${\tt ,}~$B$''. The non dependent
-product is used both to denote the propositional implication and
+$B$'' stands for ``{\tt forall \_:}$A${\tt ,}~$B$''. The {\em non dependent
+product} is used both to denote the propositional implication and
 function types.
 
 \subsection{Applications