Imported Upstream version 8.4~betaupstream/8.4_beta

1 files changed, 1 insertions, 14 deletions

diff --git a/test-suite/output/Fixpoint.out b/test-suite/output/Fixpoint.out
index c69d31f4..a13ae462 100644
--- a/test-suite/output/Fixpoint.out
+++ b/test-suite/output/Fixpoint.out
@@ -9,17 +9,4 @@ 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.
- 
+Ltac f id1 id2 := fix id1 2 with (id2 (n:_) (H:odd n) {struct H} : n >= 1)