Minor fix in doc chapter on inference rules (added a missing space).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13029 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 2 insertions, 2 deletions

diff --git a/doc/refman/RefMan-cic.tex b/doc/refman/RefMan-cic.tex
index 4d473d54b6..9660a04bd5 100644
--- a/doc/refman/RefMan-cic.tex
+++ b/doc/refman/RefMan-cic.tex
@@ -1225,8 +1225,8 @@ $I$.
 
 \begin{description}
 \item[Prod] \inference{\frac{\compat{(I~x):A'}{B'}}
-                      {\compat{I:(x:A)A'}{(x:A)B'}}}
-\item[\Set \& \Type] \inference{\frac{
+                      {\compat{I:\forall x:A, A'}{\forall x:A, B'}}}
+\item[{\Set} \& \Type] \inference{\frac{
     s_1 \in \{\Set,\Type(j)\}, 
     s_2 \in \Sort}{\compat{I:s_1}{I\ra s_2}}}
 \end{description}