From b9c75963bccb690e16207f9fe4ce23c5e9318ee6 Mon Sep 17 00:00:00 2001
From: Tanaka Akira
Date: Mon, 11 Feb 2019 14:43:40 +0900
Subject: Use {LEFT,RIGHT} DOUBLE QUOTATION MARK.

Use LEFT DOUBLE QUOTATION MARK (U+201C) and
RIGHT DOUBLE QUOTATION MARK (U+201D) instead of
QUOTATION MARK (U+0022).

QUOTATION MARK is formatted as same form both for
opening and closing quotation mark.
---
 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 acee27107b..8919bfc582 100644
--- a/doc/sphinx/language/cic.rst
+++ b/doc/sphinx/language/cic.rst
@@ -20,7 +20,7 @@ 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
+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”.
 
-- 
cgit v1.2.3