Revert "Add #[uniform] and #[nonuniform] (for Uniform Inductive Parameters)"

This reverts commit bc2c1836ba4c878903288060bcb66a0ef1aaced6.

3 files changed, 18 insertions, 38 deletions

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.
 
diff --git a/test-suite/success/uniform_inductive_parameters.v b/test-suite/success/uniform_inductive_parameters.v
index 651247937d..42236a5313 100644
--- a/test-suite/success/uniform_inductive_parameters.v
+++ b/test-suite/success/uniform_inductive_parameters.v
@@ -1,23 +1,13 @@
-Module Att.
-  #[uniform] Inductive list (A : Type) :=
-  | nil : list
-  | cons : A -> list -> list.
-  Check (list : Type -> Type).
-  Check (cons : forall A, A -> list A -> list A).
-End Att.
-
 Set Uniform Inductive Parameters.
 
 Inductive list (A : Type) :=
-| nil : list
-| cons : A -> list -> list.
+  | nil : list
+  | cons : A -> list -> list.
 Check (list : Type -> Type).
 Check (cons : forall A, A -> list A -> list A).
 
 Inductive list2 (A : Type) (A' := prod A A) :=
-| nil2 : list2
-| cons2 : A' -> list2 -> list2.
+  | nil2 : list2
+  | cons2 : A' -> list2 -> list2.
 Check (list2 : Type -> Type).
 Check (cons2 : forall A (A' := prod A A), A' -> list2 A -> list2 A).
-
-#[nonuniform] Inductive bla (n:nat) := c (_ : bla (S n)).
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index e469323f50..dec5a79892 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -623,18 +623,16 @@ let should_treat_as_cumulative cum poly =
     else user_err Pp.(str "The NonCumulative prefix can only be used in a polymorphic context.")
   | None -> poly && is_polymorphic_inductive_cumulativity ()
 
-let uniform_att =
-  let get_uniform_inductive_parameters =
-    Goptions.declare_bool_option_and_ref
-      ~depr:false
-      ~key:["Uniform"; "Inductive"; "Parameters"]
-      ~value:false
-  in
-  let open Attributes.Notations in
-  Attributes.bool_attribute ~name:"uniform" ~on:"uniform" ~off:"nonuniform" >>= fun u ->
-  let u = match u with Some u -> u | None -> get_uniform_inductive_parameters () in
-  let u = if u then ComInductive.UniformParameters else ComInductive.NonUniformParameters in
-  return u
+let get_uniform_inductive_parameters =
+  Goptions.declare_bool_option_and_ref
+    ~depr:false
+    ~key:["Uniform"; "Inductive"; "Parameters"]
+    ~value:false
+
+let should_treat_as_uniform () =
+  if get_uniform_inductive_parameters ()
+  then ComInductive.UniformParameters
+  else ComInductive.NonUniformParameters
 
 let vernac_record ~template udecl cum k poly finite records =
   let cumulative = should_treat_as_cumulative cum poly in
@@ -682,6 +680,7 @@ let finite_of_kind = let open Declarations in function
     indicates whether the type is inductive, co-inductive or
     neither. *)
 let vernac_inductive ~atts cum lo kind indl =
+  let template, poly = Attributes.(parse Notations.(template ++ polymorphic) atts) in
   let open Pp in
   let udecl, indl = extract_inductive_udecl indl in
   if Dumpglob.dump () then
@@ -713,9 +712,7 @@ let vernac_inductive ~atts cum lo kind indl =
     let (coe, (lid, ce)) = l in
     let coe' = if coe then Some true else None in
     let f = AssumExpr ((make ?loc:lid.loc @@ Name lid.v), ce),
-            { rf_subclass = coe' ; rf_priority = None ; rf_notation = [] ; rf_canonical = true }
-    in
-    let template, poly = Attributes.(parse Notations.(template ++ polymorphic) atts) in
+            { rf_subclass = coe' ; rf_priority = None ; rf_notation = [] ; rf_canonical = true } in
     vernac_record ~template udecl cum (Class true) poly finite [id, bl, c, None, [f]]
   else if List.for_all is_record indl then
     (* Mutual record case *)
@@ -737,7 +734,6 @@ let vernac_inductive ~atts cum lo kind indl =
     in
     let kind = match kind with Class _ -> Class false | _ -> kind in
     let recordl = List.map unpack indl in
-    let template, poly = Attributes.(parse Notations.(template ++ polymorphic) atts) in
     vernac_record ~template udecl cum kind poly finite recordl
   else if List.for_all is_constructor indl then
     (* Mutual inductive case *)
@@ -761,12 +757,9 @@ let vernac_inductive ~atts cum lo kind indl =
     | RecordDecl _ -> assert false (* ruled out above *)
     in
     let indl = List.map unpack indl in
-    let (template, poly), uniform =
-      Attributes.(parse Notations.(template ++ polymorphic ++ uniform_att) atts)
-    in
     let cumulative = should_treat_as_cumulative cum poly in
-    ComInductive.do_mutual_inductive ~template udecl indl ~cumulative ~poly
-      ~private_ind:lo ~uniform finite
+    let uniform = should_treat_as_uniform () in
+    ComInductive.do_mutual_inductive ~template udecl indl ~cumulative ~poly ~private_ind:lo ~uniform finite
   else
     user_err (str "Mixed record-inductive definitions are not allowed")