Change parameters p_1...p_r to q_1...q_r.

In the description of destructors,
"Type of branches" section and "Typing rule" section shares
the definition of "r" (and "s" from previous commit).

However actual parameters are p_1...p_r in the former section and
q_1...q_r in the latter section.

I guess it's because the latter section uses
p_1...p_l in other purpose: index of constructor for a inductive type.

So, I change the parameter p_1...p_r to q_1...q_r in the former section
to consistent with the latter section.

1 files changed, 1 insertions, 1 deletions

diff --git a/doc/sphinx/language/cic.rst b/doc/sphinx/language/cic.rst
index 21ec62dd70..a3fa12c618 100644
--- a/doc/sphinx/language/cic.rst
+++ b/doc/sphinx/language/cic.rst
@@ -1449,7 +1449,7 @@ corresponding to the :math:`c:C` constructor.
 
 .. math::
    \begin{array}{ll}
-   \{c:(I~p_1\ldots p_r\ t_1 \ldots t_s)\}^P &\equiv (P~t_1\ldots ~t_s~c) \\
+   \{c:(I~q_1\ldots q_r\ t_1 \ldots t_s)\}^P &\equiv (P~t_1\ldots ~t_s~c) \\
    \{c:∀ x:T,~C\}^P &\equiv ∀ x:T,~\{(c~x):C\}^P
    \end{array}