From 3e9c1312250acd4b1e791d5d35ce6581cbe30caf Mon Sep 17 00:00:00 2001
From: Tanaka Akira
Date: Mon, 11 Feb 2019 15:02:59 +0900
Subject: Use math mode more.

Also quoted parts are emphasized as coq-8.7.2-reference-manual.pdf.
And two "x:T" are quoted.
---
 doc/sphinx/language/cic.rst | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'doc')

diff --git a/doc/sphinx/language/cic.rst b/doc/sphinx/language/cic.rst
index 8919bfc582..df6d433051 100644
--- a/doc/sphinx/language/cic.rst
+++ b/doc/sphinx/language/cic.rst
@@ -20,9 +20,9 @@ There are types for functions (or programs), there are atomic types
 (especially datatypes)... but also types for proofs and types for the
 types themselves. Especially, any object handled in the formalism must
 belong to a type. For instance, universal quantification is relative
-to a type and takes the form “*for all x of type T, P*”. The expression
-“x of type T” is written :g:`x:T`. Informally, :g:`x:T` can be thought as
-“x belongs to T”.
+to a type and takes the form “*for all x of type* :math:`T`, :math:`P`”. The expression
+“:math:`x` *of type* :math:`T`” is written “:math:`x:T`”. Informally, “:math:`x:T`” can be thought as
+“:math:`x` *belongs to* :math:`T`”.
 
 The types of types are *sorts*. Types and sorts are themselves terms
 so that terms, types and sorts are all components of a common
-- 
cgit v1.2.3