diff options
| -rw-r--r-- | doc/refman/RefMan-cic.tex | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/doc/refman/RefMan-cic.tex b/doc/refman/RefMan-cic.tex index cc69355d4a..8f03cafd14 100644 --- a/doc/refman/RefMan-cic.tex +++ b/doc/refman/RefMan-cic.tex @@ -760,7 +760,9 @@ $\begin{array}{@{} l} \subsection{Well-formed inductive definitions} We cannot accept any inductive declaration because some of them lead -to inconsistent systems. We restrict ourselves to definitions which +to inconsistent systems. +% TODO: The statement above deserves explanation. +We restrict ourselves to definitions which satisfy a syntactic criterion of positivity. Before giving the formal rules, we need a few definitions: |