From ee629d65f2d36544b0e5c8afb657933ef19c296d Mon Sep 17 00:00:00 2001
From: Matej Kosik
Date: Tue, 3 Nov 2015 11:40:20 +0100
Subject: COMMENT: question

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

(limited to 'doc/refman')

diff --git a/doc/refman/RefMan-cic.tex b/doc/refman/RefMan-cic.tex
index 5df70a8e97..45613e03af 100644
--- a/doc/refman/RefMan-cic.tex
+++ b/doc/refman/RefMan-cic.tex
@@ -312,6 +312,7 @@ be derived from the following rules.
 \item[W-Local-Def]
 \inference{\frac{\WTEG{t}{T}~~~~x \not\in \Gamma % \cup E
      }{\WFE{\Gamma::(x:=t:T)}}}
+% QUESTION: Why in W-Global-Assum and W-Global-Def we do not need x ∉ Γ hypothesis?
 \item[W-Global-Assum] \inference{\frac{\WTE{}{T}{s}~~~~s \in \Sort~~~~c \notin E}
                       {\WF{E;c:T}{}}}
 \item[W-Global-Def] \inference{\frac{\WTE{}{t}{T}~~~c \notin E}
-- 
cgit v1.2.3