1 files changed, 4 insertions, 14 deletions
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)).