Merge PR #7703: Add an option to force parameters to be uniform

1 files changed, 13 insertions, 0 deletions

diff --git a/test-suite/success/uniform_inductive_parameters.v b/test-suite/success/uniform_inductive_parameters.v
new file mode 100644
index 0000000000..42236a5313
--- /dev/null
+++ b/test-suite/success/uniform_inductive_parameters.v
@@ -0,0 +1,13 @@
+Set Uniform Inductive Parameters.
+
+Inductive list (A : Type) :=
+  | 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.
+Check (list2 : Type -> Type).
+Check (cons2 : forall A (A' := prod A A), A' -> list2 A -> list2 A).