From ad13db81f25f48d1a0c800b16200426003c08b07 Mon Sep 17 00:00:00 2001
From: Tanaka Akira
Date: Thu, 31 Jan 2019 16:37:59 +0900
Subject: \Sort is not a term.

"∀Γ_P ,∀Γ_{\mathit{Arr}(t)}, \Sort" is changed to
"∀Γ_P ,∀Γ_{\mathit{Arr}(t)}, S" because
\Sort is not a term.
"S" is choosen to be consistent with the description of
Inductive Definitions.
---
 doc/sphinx/language/cic.rst | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'doc')

diff --git a/doc/sphinx/language/cic.rst b/doc/sphinx/language/cic.rst
index 030214fe46..d63adf218d 100644
--- a/doc/sphinx/language/cic.rst
+++ b/doc/sphinx/language/cic.rst
@@ -618,9 +618,9 @@ a *subtyping* relation inductively defined by:
 #. if :math:`\ind{p}{Γ_I}{Γ_C}` is a universe polymorphic and cumulative
    (see Chapter :ref:`polymorphicuniverses`) inductive type (see below)
    and
-   :math:`(t : ∀Γ_P ,∀Γ_{\mathit{Arr}(t)}, \Sort)∈Γ_I`
+   :math:`(t : ∀Γ_P ,∀Γ_{\mathit{Arr}(t)}, S)∈Γ_I`
    and
-   :math:`(t' : ∀Γ_P' ,∀Γ_{\mathit{Arr}(t)}', \Sort')∈Γ_I`
+   :math:`(t' : ∀Γ_P' ,∀Γ_{\mathit{Arr}(t)}', S')∈Γ_I`
    are two different instances of *the same* inductive type (differing only in
    universe levels) with constructors
 
-- 
cgit v1.2.3