From 678f41f598f38c9c0ef7c587f7b876437a6d06d8 Mon Sep 17 00:00:00 2001
From: Matej Kosik
Date: Thu, 29 Oct 2015 15:02:04 +0100
Subject: COMMENT: question

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

diff --git a/doc/refman/RefMan-cic.tex b/doc/refman/RefMan-cic.tex
index 1804ebd9ce..56e9a27790 100644
--- a/doc/refman/RefMan-cic.tex
+++ b/doc/refman/RefMan-cic.tex
@@ -312,6 +312,7 @@ be derived from the following rules.
                       {\WF{E;c:T}{}}}
 \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.
 \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