From fcb4cf7628ea67cf342f8c39cb7f5151897ff72c Mon Sep 17 00:00:00 2001
From: Tanaka Akira
Date: Thu, 31 Jan 2019 19:00:55 +0900
Subject: Use "U" instead of "u" for a type.

---
 doc/sphinx/language/cic.rst | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'doc')

diff --git a/doc/sphinx/language/cic.rst b/doc/sphinx/language/cic.rst
index 2c8074be69..e3fd543c93 100644
--- a/doc/sphinx/language/cic.rst
+++ b/doc/sphinx/language/cic.rst
@@ -1658,7 +1658,7 @@ Given a variable :math:`y` of an inductively defined type in a declaration
 :math:`[c_1 :C_1 ;~…;~c_n :C_n ]`, the terms structurally smaller than :math:`y` are:
 
 
-+ :math:`(t~u)` and :math:`λ x:u .~t` when :math:`t` is structurally smaller than :math:`y`.
++ :math:`(t~u)` and :math:`λ x:U .~t` when :math:`t` is structurally smaller than :math:`y`.
 + :math:`\case(c,P,f_1 … f_n)` when each :math:`f_i` is structurally smaller than :math:`y`.
   If :math:`c` is :math:`y` or is structurally smaller than :math:`y`, its type is an inductive
   definition :math:`I_p` part of the inductive declaration corresponding to :math:`y`.
-- 
cgit v1.2.3