From 4165cce72347466fbaa565247ae040a873b46694 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Fri, 14 Feb 2020 10:53:10 +0100
Subject: Revert "Add #[uniform] and #[nonuniform] (for Uniform Inductive
 Parameters)"

This reverts commit bc2c1836ba4c878903288060bcb66a0ef1aaced6.
---
 doc/sphinx/language/gallina-specification-language.rst | 3 ---
 1 file changed, 3 deletions(-)

(limited to 'doc/sphinx')

diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst
index 721c7a7a51..09090ce89a 100644
--- a/doc/sphinx/language/gallina-specification-language.rst
+++ b/doc/sphinx/language/gallina-specification-language.rst
@@ -1063,9 +1063,6 @@ 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