Imported Upstream version 8.2~beta3+dfsgupstream/8.2.beta3+dfsg

1 files changed, 14 insertions, 0 deletions

diff --git a/test-suite/output/Fixpoint.out b/test-suite/output/Fixpoint.out
index 62c9d395..f4270d3d 100644
--- a/test-suite/output/Fixpoint.out
+++ b/test-suite/output/Fixpoint.out
@@ -9,3 +9,17 @@ let fix f (m : nat) : nat := match m with
                              | S m' => f m'
                              end in f 0
      : nat
+fix even_pos_odd_pos 2
+ with (odd_pos_even_pos (n:_) (H:odd n) {struct H} : n >= 1).
+ intros.
+ destruct H.
+   omega.
+  
+   apply odd_pos_even_pos in H.
+   omega.
+  
+ intros.
+ destruct H.
+  apply even_pos_odd_pos in H.
+  omega.
+