From 435cd91ddb71a59fef3611210b19e9d01fc730f9 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 21 Sep 2014 21:11:45 +0200
Subject: Documenting option -type-in-type.

---
 doc/refman/RefMan-com.tex | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'doc')

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}
-- 
cgit v1.2.3