Documenting option -type-in-type.

2 files changed, 8 insertions, 0 deletions

diff --git a/CHANGES b/CHANGES
index c03e30bdfe..4ba66a4085 100644
--- a/CHANGES
+++ b/CHANGES
@@ -32,6 +32,10 @@ Logic
     projection application.
   - [pattern x at n], [rewrite x at n] and in general abstraction and selection
     of occurrences may fail due to the disappearance of parameters.
+- New universe polymorphism.
+- New option -type-in-type to collapse the universe hierarchy (this makes the
+  logic inconsistent).
+
 
 Vernacular commands
 
diff --git a/doc/refman/RefMan-com.tex b/doc/refman/RefMan-com.tex
index 56cf8b06a7..8d128e6b47 100644
--- a/doc/refman/RefMan-com.tex
+++ b/doc/refman/RefMan-com.tex
@@ -193,6 +193,10 @@ Add physical path {\em directory} to the {\ocaml} loadpath.
   some standard axioms of classical mathematics such as the functional
   axiom of choice or the principle of description
 
+\item[{\tt -type-in-type}]\
+
+  This collapses the universe hierarchy of {\Coq} making the logic inconsistent.
+
 \item[{\tt -compat} {\em version}] \mbox{}
 
   Attempt to maintain some of the incompatible changes in their {\em version}