diff options
| author |  Matej Kosik <m4tej.kosik@gmail.com> | 2015-11-05 17:23:45 +0100 |
|---|---|---|
| committer |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-12-10 09:35:16 +0100 |
| commit | c3973cc972cd1474fb4bad308197d64634a518dc (patch) | |
| tree | 7f8da62b5f7b96832815996f9e64e69656f5f795 /doc/refman | |
| parent | 6a54c04d60038fbf5b617ee76bb59216ff4038d4 (diff) | |
COMMENT: question
Diffstat (limited to 'doc/refman')
| -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 611782b4f..9e11d66ab 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} |