From 5e48f1aafb45d1c883e32e13a8458979663b04fb Mon Sep 17 00:00:00 2001
From: Matej Kosik
Date: Mon, 9 Nov 2015 16:52:23 +0100
Subject: PROPOSITION: Added "if" and "then" words missing in the original
 sentence.

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

(limited to 'doc')

diff --git a/doc/refman/RefMan-cic.tex b/doc/refman/RefMan-cic.tex
index ac860b8276..6c1417a7f2 100644
--- a/doc/refman/RefMan-cic.tex
+++ b/doc/refman/RefMan-cic.tex
@@ -1622,10 +1622,10 @@ The definition of being structurally smaller is a bit technical.
 One needs first to  define the notion of 
 {\em recursive arguments of a constructor}\index{Recursive arguments}.
 For an inductive definition \Ind{}{r}{\Gamma_I}{\Gamma_C},
-the type of a constructor $c$ has the form
+if the type of a constructor $c$ has the form
 $\forall p_1:P_1,\ldots \forall p_r:P_r, 
 \forall x_1:T_1, \ldots \forall x_r:T_r, (I_j~p_1\ldots 
-p_r~t_1\ldots  t_s)$ the recursive arguments will correspond to $T_i$ in
+p_r~t_1\ldots  t_s)$, then the recursive arguments will correspond to $T_i$ in
 which one of the $I_l$ occurs.
 
 The main rules for being structurally smaller are the following:\\
-- 
cgit v1.2.3