From 7dc6dfee7eb641282f4268aea24c688da07470ee Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Fri, 13 Feb 2015 20:13:33 +0100
Subject: Document the issue with trivial inductive types. (Workaround for bug
 #3984)

---
 CHANGES | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/CHANGES b/CHANGES
index ca31ca2398..7f134679fc 100644
--- a/CHANGES
+++ b/CHANGES
@@ -22,6 +22,10 @@ Logic
   the return predicate. Restores compatibility of Coq's logic with the
   propositional extensionality axiom. May create incompatibilities in
   recursive programs heavily using dependent types.
+- Trivial inductive types are no longer defined in Type but in Prop, which
+  leads to a non-dependent induction principle being generated in place of
+  the dependent one. To recover the old behavior, explicitly define your
+  inductive types in Set.
 
 Vernacular commands
 
-- 
cgit v1.2.3