diff options
| -rw-r--r-- | doc/refman/RefMan-cic.tex | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/doc/refman/RefMan-cic.tex b/doc/refman/RefMan-cic.tex index 611782b4f6..9e11d66ab5 100644 --- a/doc/refman/RefMan-cic.tex +++ b/doc/refman/RefMan-cic.tex @@ -1464,6 +1464,7 @@ predicate $P$ of type $I\ra \Type$ leads to a paradox when applied to impredicative inductive definition like the second-order existential quantifier \texttt{exProp} defined above, because it give access to the two projections on this type. +% QUESTION: I did not get the point of the paragraph above. %\paragraph{Warning: strong elimination} %\index{Elimination!Strong elimination} |