From 5edfac63b6feb0b8d6ddad47a4ca9c8b5905b03a Mon Sep 17 00:00:00 2001
From: Matej Kosik
Date: Wed, 4 Nov 2015 19:31:05 +0100
Subject: COMMENT: questions

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

diff --git a/doc/refman/RefMan-cic.tex b/doc/refman/RefMan-cic.tex
index ddd9f075ef..b862db3204 100644
--- a/doc/refman/RefMan-cic.tex
+++ b/doc/refman/RefMan-cic.tex
@@ -1910,7 +1910,36 @@ impredicative system for sort \Set{} become:
          {\compat{I:\Set}{I\ra s}}}
 \end{description}
      
+% QUESTION: Why, when I add this definition:
+%
+%   Inductive foo : Type := .
+%
+% Coq claims that the type of 'foo' is 'Prop'?
+
+% QUESTION: If I add this definition:
+%
+%   Inductive bar (A:Type) : Type := .
+%
+% then Coq claims that 'bar' has type 'Type → Prop' where I would expect 'Type → Type' with appropriate constraint.
 
+% QUESTION: If I add this definition:
+%
+%   Inductive foo (A:Type) : Type :=
+%   | foo1 : foo A
+%   | foo2 : foo A.
+%
+% then Coq claims that 'foo' has type 'Type → Set'.
+% Why?
+
+% NOTE: If I add this definition:
+%
+%   Inductive foo (A:Type) : Type :=
+%   | foo1 : foo A
+%   | foo2 : A → foo A.
+%
+% then Coq claims, as expected, that:
+%
+%   foo : Type → Type.
 
 %%% Local Variables: 
 %%% mode: latex
-- 
cgit v1.2.3