From 0a25e351d6a2d25e5d82b165843a09a2804fadc6 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Mon, 17 Sep 2018 11:14:18 +0200
Subject: Add CHANGES for auto-template warning.

---
 CHANGES.md | 11 +++++++++++
 1 file changed, 11 insertions(+)

diff --git a/CHANGES.md b/CHANGES.md
index d64b5accd7..b8c0068778 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -135,6 +135,17 @@ Universes
   for the "Private Polymorphic Universes" option (and Unset it to get
   the previous behaviour).
 
+Inductives
+
+- An option and attributes to control the automatic decision to
+  declare an inductive type as template polymorphic were added.
+  Warning "auto-template" will trigger when an inductive is
+  automatically declared template polymorphic without the attribute.
+
+Funind
+
+- Inductive types declared by Funind will never be template polymorphic.
+
 Misc
 
 - Option "Typeclasses Axioms Are Instances" is deprecated. Use Declare Instance for axioms which should be instances.
-- 
cgit v1.2.3