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.

---
 CHANGES                   | 4 ++++
 doc/refman/RefMan-com.tex | 4 ++++
 2 files changed, 8 insertions(+)

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