From 9995c44df32858624a84a5f87f14a4a24124f84e Mon Sep 17 00:00:00 2001
From: Tanaka Akira
Date: Wed, 30 Sep 2020 02:44:24 +0900
Subject: Type{i} should be Type(i).

---
 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 768c83150e..f1ed64e52a 100644
--- a/doc/sphinx/language/cic.rst
+++ b/doc/sphinx/language/cic.rst
@@ -274,7 +274,7 @@ following rules.
 .. inference:: Prod-Type
 
    \WTEG{T}{s}
-   s \in \{\SProp, \Type{i}\}
+   s \in \{\SProp, \Type(i)\}
    \WTE{\Gamma::(x:T)}{U}{\Type(i)}
    --------------------------------
    \WTEG{∀ x:T,~U}{\Type(i)}
-- 
cgit v1.2.3