From 289dde7331ee19229b9ba4b9778a76007d93b275 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 19 Oct 2015 10:55:19 +0200
Subject: Documenting the option "Strict Universe Declaration" in CHANGES.

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

diff --git a/CHANGES b/CHANGES
index 07d129a462..9f46131363 100644
--- a/CHANGES
+++ b/CHANGES
@@ -5,6 +5,9 @@ Vernacular commands
 
 - New command "Redirect" to redirect the output of a command to a file.
 - New command "Undelimit Scope" to remove the delimiter of a scope.
+- New option "Strict Universe Declaration", set by default. It enforces the
+  declaration of all polymorphic universes appearing in a definition when
+  introducing it.
 
 Tactics
 
-- 
cgit v1.2.3