1 files changed, 52 insertions, 7 deletions
diff --git a/test-suite/success/fix.v b/test-suite/success/fix.v
index f4a4d36d..78b01f3e 100644
--- a/test-suite/success/fix.v
+++ b/test-suite/success/fix.v
@@ -1,10 +1,3 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
 (* Ancien bug signale par Laurent Thery sur la condition de garde *)
 
 Require Import Bool.
@@ -50,3 +43,55 @@ Fixpoint maxVar (e : rExpr) : rNat :=
   | rNode n p q => rmax (maxVar p) (maxVar q)
   end.
 
+(* Check bug #1491 *)
+
+Require Import Streams.
+
+Definition decomp (s:Stream nat) : Stream nat := 
+  match s with Cons _ s => s end.
+
+CoFixpoint bx0 : Stream nat := Cons 0 bx1 
+with bx1 : Stream nat := Cons 1 bx0.
+
+Lemma bx0bx : decomp bx0 = bx1.
+simpl. (* used to return bx0 in V8.1 and before instead of bx1 *)
+reflexivity.
+Qed.
+
+(* Check mutually inductive statements *)
+
+Require Import ZArith_base Omega.
+Open Scope Z_scope.
+
+Inductive even: Z -> Prop :=
+| even_base: even 0
+| even_succ: forall n, odd (n - 1) -> even n
+with odd: Z -> Prop :=
+| odd_succ: forall n, even (n - 1) -> odd n.
+
+Lemma even_pos_odd_pos: forall n, even n -> n >= 0
+with odd_pos_even_pos : forall n, odd n -> n >= 1.
+Proof.
+ intros.
+ destruct H.
+   omega.
+   apply odd_pos_even_pos in H.
+   omega.
+ intros.
+ destruct H.
+  apply even_pos_odd_pos in H.
+  omega.
+Qed.
+
+CoInductive a : Prop := acons : b -> a
+with b : Prop := bcons : a -> b.
+
+Lemma a1 : a
+with b1 : b.
+Proof.
+apply acons.
+assumption.
+
+apply bcons.
+assumption.
+Qed.