Imported Upstream snapshot 8.3~beta0+13298

1 files changed, 15 insertions, 0 deletions

diff --git a/test-suite/success/autointros.v b/test-suite/success/autointros.v
new file mode 100644
index 00000000..0a081271
--- /dev/null
+++ b/test-suite/success/autointros.v
@@ -0,0 +1,15 @@
+Set Automatic Introduction.
+
+Inductive even : nat -> Prop :=
+| even_0 : even 0
+| even_odd : forall n, odd n -> even (S n)
+with odd : nat -> Prop :=
+| odd_1 : odd 1
+| odd_even : forall n, even n -> odd (S n).
+
+Lemma foo {n : nat} (E : even n) : even (S (S n))
+with bar {n : nat} (O : odd n) : odd (S (S n)).
+Proof. destruct E. constructor. constructor. apply even_odd. apply (bar _ H).
+  destruct O. repeat constructor. apply odd_even. apply (foo _ H).
+Defined.
+