From 70e705a47f435e1453d889177a426d89dacda07b Mon Sep 17 00:00:00 2001
From: Matej Kosik
Date: Wed, 4 Nov 2015 18:54:17 +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 00ba0091ee..1013084702 100644
--- a/doc/refman/RefMan-cic.tex
+++ b/doc/refman/RefMan-cic.tex
@@ -969,6 +969,10 @@ the type $V$ satisfies the nested positivity condition for $X$
 \end{latexonly}
 
 \paragraph{Correctness rules.}
+% QUESTION: For a related problem, in case of global definitions
+% and global assumptions, we used the term "well-formedness".
+% Couldn't we continue to use the term also here?
+% Does it make sense to use a different name, i.e. "correctness" in this case?
 We shall now describe the rules allowing the introduction of a new
 inductive definition.
 
-- 
cgit v1.2.3