diff options
Diffstat (limited to 'test-suite/success/uniform_inductive_parameters.v')
-rw-r--r-- | test-suite/success/uniform_inductive_parameters.v | 13 |
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 00000000..42236a53 --- /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). |