diff options
| -rw-r--r-- | test-suite/success/Fixpoint.v | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/test-suite/success/Fixpoint.v b/test-suite/success/Fixpoint.v index fcf8d8d4a7..3a4f88993f 100644 --- a/test-suite/success/Fixpoint.v +++ b/test-suite/success/Fixpoint.v @@ -50,6 +50,8 @@ End folding. (* Check definition by tactics *) +Set Automatic Introduction. + Inductive even : nat -> Type := | even_O : even 0 | even_S : forall n, odd n -> even (S n) |