From e13fed125d22e58e39487a3aa227416e1f2ba329 Mon Sep 17 00:00:00 2001
From: Matej Kosik
Date: Thu, 29 Oct 2015 15:13:25 +0100
Subject: COMMENT: question

---
 doc/refman/RefMan-cic.tex | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/doc/refman/RefMan-cic.tex b/doc/refman/RefMan-cic.tex
index 56e9a27790..22cec45cc2 100644
--- a/doc/refman/RefMan-cic.tex
+++ b/doc/refman/RefMan-cic.tex
@@ -313,6 +313,10 @@ be derived from the following rules.
 \item[W-Global-Def] \inference{\frac{\WTE{}{t}{T}~~~c \notin E}
                       {\WF{E;c:=t:T}{}}}
 % QUESTION: Why, in case of W-Local-Assum and W-Global-Assum we need s ∈ S hypothesis.
+% QUESTION: At the moment, enrichment of a local context is denoted with ∷
+%           whereas enrichment of the global environment is denoted with ;
+%           Is it necessary to use two different notations?
+%           Couldn't we use ∷ also for enrichment of the global context?
 \item[Ax] \index{Typing rules!Ax}
 \inference{\frac{\WFE{\Gamma}}{\WTEG{\Prop}{\Type(1)}}~~~~~
 \frac{\WFE{\Gamma}}{\WTEG{\Set}{\Type(1)}}}
-- 
cgit v1.2.3