Documenting the option "Strict Universe Declaration" in CHANGES.

1 files changed, 3 insertions, 0 deletions

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