New syntax [Inductive Acc A R | x : Prop := ...]

to control uniform parameters.

This replaces the attribute.

1 files changed, 9 insertions, 0 deletions

diff --git a/test-suite/success/uniform_inductive_parameters.v b/test-suite/success/uniform_inductive_parameters.v
index 42236a5313..e2b4694fff 100644
--- a/test-suite/success/uniform_inductive_parameters.v
+++ b/test-suite/success/uniform_inductive_parameters.v
@@ -11,3 +11,12 @@ Inductive list2 (A : Type) (A' := prod A A) :=
   | cons2 : A' -> list2 -> list2.
 Check (list2 : Type -> Type).
 Check (cons2 : forall A (A' := prod A A), A' -> list2 A -> list2 A).
+
+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.