From e46ce40cee2c34f47acb55d2b24bd09f00987556 Mon Sep 17 00:00:00 2001
From: xclerc
Date: Fri, 20 Sep 2013 12:40:28 +0000
Subject: Get rid of "shouldsucceed" subdirectory by moving tests to parent
 directory.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16797 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 test-suite/bugs/closed/2089.v | 17 +++++++++++++++++
 1 file changed, 17 insertions(+)
 create mode 100644 test-suite/bugs/closed/2089.v

(limited to 'test-suite/bugs/closed/2089.v')

diff --git a/test-suite/bugs/closed/2089.v b/test-suite/bugs/closed/2089.v
new file mode 100644
index 0000000000..aebccc9424
--- /dev/null
+++ b/test-suite/bugs/closed/2089.v
@@ -0,0 +1,17 @@
+Inductive even (x: nat): nat -> Prop :=
+  | even_base: even x O
+  | even_succ: forall n, odd x n -> even x (S n)
+
+with odd (x: nat): nat -> Prop :=
+  | odd_succ: forall n, even x n -> odd x (S n).
+
+Scheme even_ind2 := Minimality for even Sort Prop
+  with odd_ind2 := Minimality for odd Sort Prop.
+
+Combined Scheme even_odd_ind from even_ind2, odd_ind2.
+
+Check (even_odd_ind :forall (x : nat) (P P0 : nat -> Prop),
+  P 0 ->
+  (forall n : nat, odd x n -> P0 n -> P (S n)) ->
+  (forall n : nat, even x n -> P n -> P0 (S n)) ->
+  (forall n : nat, even x n -> P n) /\ (forall n : nat, odd x n -> P0 n)).
-- 
cgit v1.2.3