Merge PR #11600: New syntax [Inductive Acc A R | x : Prop := ...]

Reviewed-by: Zimmi48
Reviewed-by: maximedenes
Reviewed-by: ppedrot

1 files changed, 12 insertions, 13 deletions

diff --git a/test-suite/success/uniform_inductive_parameters.v b/test-suite/success/uniform_inductive_parameters.v
index 651247937d..e2b4694fff 100644
--- a/test-suite/success/uniform_inductive_parameters.v
+++ b/test-suite/success/uniform_inductive_parameters.v
@@ -1,23 +1,22 @@
-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)).
+Inductive list3 | A := nil3 | cons3 : A -> list3 (A * A)%type -> list3 A.
+
+Unset Uniform Inductive Parameters.
+
+Inductive list4 A | := nil4 | cons4 : A -> list4 -> list4.
+
+Inductive Acc {A:Type} (R:A->A->Prop) | (x:A) : Prop
+  := Acc_in : (forall y, R y x -> Acc y) -> Acc x.