From f07348e606882ddb0d69029bde82be3106335f21 Mon Sep 17 00:00:00 2001
From: Matej Kosik <m4tej.kosik@gmail.com>
Date: Tue, 3 Nov 2015 11:39:54 +0100
Subject: COMMENT: question

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

(limited to 'doc')

diff --git a/doc/refman/RefMan-cic.tex b/doc/refman/RefMan-cic.tex
index f7a6470f9..5df70a8e9 100644
--- a/doc/refman/RefMan-cic.tex
+++ b/doc/refman/RefMan-cic.tex
@@ -305,6 +305,7 @@ local context $\Gamma$ and a term $T$ such that the judgment \WTEG{t}{T} can
 be derived from the following rules.
 \begin{description}
 \item[W-Empty] \inference{\WF{[]}{}}
+% QUESTION: Why in W-Local-Assum and W-Local-Def we do not need x ∉ E hypothesis?
 \item[W-Local-Assum]  % Ce n'est pas vrai : x peut apparaitre plusieurs fois dans Gamma
 \inference{\frac{\WTEG{T}{s}~~~~s \in \Sort~~~~x \not\in \Gamma % \cup E
       }{\WFE{\Gamma::(x:T)}}}
-- 
cgit v1.2.3