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

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

1 files changed, 14 insertions, 4 deletions

diff --git a/test-suite/success/uniform_inductive_parameters.v b/test-suite/success/uniform_inductive_parameters.v
index 42236a5313..651247937d 100644
--- a/test-suite/success/uniform_inductive_parameters.v
+++ b/test-suite/success/uniform_inductive_parameters.v
@@ -1,13 +1,23 @@
+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)).