diff options
| -rw-r--r-- | doc/refman/RefMan-cic.tex | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/doc/refman/RefMan-cic.tex b/doc/refman/RefMan-cic.tex index 8c8537cfb2..1a17f3f35f 100644 --- a/doc/refman/RefMan-cic.tex +++ b/doc/refman/RefMan-cic.tex @@ -1764,7 +1764,9 @@ $\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 which one of the $I_l$ occurs. - +% QUESTION: The last sentence above really fully make sense. +% Isn't some word missing? +% Maybe "if"? The main rules for being structurally smaller are the following:\\ Given a variable $y$ of type an inductive |