From 9b10e2383980c2f210049dfaf4a3031133d36ebd Mon Sep 17 00:00:00 2001
From: Jasper Hugunin
Date: Mon, 4 Jun 2018 17:59:10 -0700
Subject: Add test for Uniform Inductive Parameters

---
 test-suite/success/uniform_inductive_parameters.v | 13 +++++++++++++
 1 file changed, 13 insertions(+)
 create mode 100644 test-suite/success/uniform_inductive_parameters.v

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).
-- 
cgit v1.2.3