Merge PR #11584: Add #[uniform] and #[nonuniform] (for Uniform Inductive Parameters)

Reviewed-by: Matafou
Reviewed-by: Zimmi48
Reviewed-by: maximedenes

1 files changed, 3 insertions, 0 deletions

diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst
index 09090ce89a..721c7a7a51 100644
--- a/doc/sphinx/language/gallina-specification-language.rst
+++ b/doc/sphinx/language/gallina-specification-language.rst
@@ -1063,6 +1063,9 @@ Parameterized inductive types
         | cons3 : A -> list3 -> list3.
         End list3.
 
+     Attributes ``uniform`` and ``nonuniform`` respectively enable and
+     disable uniform parameters for a single inductive declaration block.
+
 .. seealso::
    Section :ref:`inductive-definitions` and the :tacn:`induction` tactic.