diff options
Diffstat (limited to 'test-suite/success')
| -rw-r--r-- | test-suite/success/uniform_inductive_parameters.v | 25 |
1 files changed, 12 insertions, 13 deletions
diff --git a/test-suite/success/uniform_inductive_parameters.v b/test-suite/success/uniform_inductive_parameters.v index 651247937d..e2b4694fff 100644 --- a/test-suite/success/uniform_inductive_parameters.v +++ b/test-suite/success/uniform_inductive_parameters.v @@ -1,23 +1,22 @@ -Module Att. - #[uniform] Inductive list (A : Type) := - | nil : list - | cons : A -> list -> list. - Check (list : Type -> Type). - Check (cons : forall A, A -> list A -> list A). -End Att. - Set Uniform Inductive Parameters. Inductive list (A : Type) := -| nil : list -| cons : A -> list -> list. + | 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. + | nil2 : list2 + | cons2 : A' -> list2 -> list2. Check (list2 : Type -> Type). Check (cons2 : forall A (A' := prod A A), A' -> list2 A -> list2 A). -#[nonuniform] Inductive bla (n:nat) := c (_ : bla (S n)). +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. |