summaryrefslogtreecommitdiff
path: root/test-suite/bugs/closed/shouldsucceed
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2009-07-04 13:28:35 +0200
committerGravatar Stephane Glondu <steph@glondu.net>2009-07-04 13:28:35 +0200
commite4282ea99c664d8d58067bee199cbbcf881b60d5 (patch)
treed4c4a873eb055c728666f367469fa26c3417793a /test-suite/bugs/closed/shouldsucceed
parenta0a94c1340a63cdb824507b973393882666ba52a (diff)
Imported Upstream version 8.2.pl1+dfsgupstream/8.2.pl1+dfsg
Diffstat (limited to 'test-suite/bugs/closed/shouldsucceed')
-rw-r--r--test-suite/bugs/closed/shouldsucceed/1905.v2
-rw-r--r--test-suite/bugs/closed/shouldsucceed/2089.v17
2 files changed, 18 insertions, 1 deletions
diff --git a/test-suite/bugs/closed/shouldsucceed/1905.v b/test-suite/bugs/closed/shouldsucceed/1905.v
index bd7fd796..fb2725c9 100644
--- a/test-suite/bugs/closed/shouldsucceed/1905.v
+++ b/test-suite/bugs/closed/shouldsucceed/1905.v
@@ -1,5 +1,5 @@
-Require Import Setoid.
+Require Import Setoid Program.
Axiom t : Set.
Axiom In : nat -> t -> Prop.
diff --git a/test-suite/bugs/closed/shouldsucceed/2089.v b/test-suite/bugs/closed/shouldsucceed/2089.v
new file mode 100644
index 00000000..aebccc94
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/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)).