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 ++++
 1 file changed, 4 insertions(+)

(limited to 'CHANGES')

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