From 3b79feaf661e8ebe6092849c9d30a5276366c01e Mon Sep 17 00:00:00 2001
From: Tanaka Akira
Date: Fri, 8 Feb 2019 14:03:59 +0900
Subject: 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.
---
 doc/sphinx/language/cic.rst | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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}
 
-- 
cgit v1.2.3