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