Documenting option -type-in-type.

1 files changed, 4 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