From bc2c1836ba4c878903288060bcb66a0ef1aaced6 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Wed, 12 Feb 2020 14:05:53 +0100
Subject: Add #[uniform] and #[nonuniform] (for Uniform Inductive Parameters)

---
 doc/sphinx/language/gallina-specification-language.rst | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'doc')

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.
 
-- 
cgit v1.2.3