diff options
Diffstat (limited to 'test-suite/success/Inductive.v')
| -rw-r--r-- | test-suite/success/Inductive.v | 9 |
1 files changed, 9 insertions, 0 deletions
diff --git a/test-suite/success/Inductive.v b/test-suite/success/Inductive.v index 3d4257543..04d92daad 100644 --- a/test-suite/success/Inductive.v +++ b/test-suite/success/Inductive.v @@ -121,3 +121,12 @@ Inductive foo1 : forall p, Prop := cc1 : foo1 0. (* Check cross inference of evars from constructors *) Inductive foo2 : forall p, Prop := cc2 : forall q, foo2 q | cc3 : foo2 0. + +(* An example with reduction removing an occurrence of the inductive type in one of its argument *) + +Inductive IND1 (A:Type) := CONS1 : IND1 ((fun x => A) IND1). + +(* This type was considered as ill-formed before March 2015, while it + could be accepted considering that the type IND1 above was accepted *) + +Inductive IND2 (A:Type) (T:=fun _ : Type->Type => A) := CONS2 : IND2 A -> IND2 (T IND2). |