From 94b4a3ca3f8100fc4d2da7f3fa27d6efce81c44b Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 11 Jul 2019 11:32:40 +0200
Subject: Adding changelog and documentation.

---
 doc/sphinx/addendum/universe-polymorphism.rst | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'doc/sphinx')

diff --git a/doc/sphinx/addendum/universe-polymorphism.rst b/doc/sphinx/addendum/universe-polymorphism.rst
index 395b5ce2d3..7e698bfb66 100644
--- a/doc/sphinx/addendum/universe-polymorphism.rst
+++ b/doc/sphinx/addendum/universe-polymorphism.rst
@@ -144,6 +144,8 @@ Many other commands support the ``Polymorphic`` flag, including:
 - ``Lemma``, ``Axiom``, and all the other “definition” keywords support
   polymorphism.
 
+- :cmd:`Section` will locally set the polymorphism flag inside the section.
+
 - ``Variables``, ``Context``, ``Universe`` and ``Constraint`` in a section support
   polymorphism. This means that the universe variables (and associated
   constraints) are discharged polymorphically over definitions that use
-- 
cgit v1.2.3