1 files changed, 52 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/2955.v b/test-suite/bugs/closed/2955.v
new file mode 100644
index 00000000..45e24b5f
--- /dev/null
+++ b/test-suite/bugs/closed/2955.v
@@ -0,0 +1,52 @@
+Require Import Coq.Arith.Arith.
+
+Module A.
+
+  Fixpoint foo (n:nat) :=
+  match n with
+  | 0 => 0
+  | S n => bar n
+  end
+
+  with bar (n:nat) :=
+  match n with
+  | 0 => 0
+  | S n => foo n
+  end.
+
+  Lemma using_foo:
+    forall (n:nat), foo n = 0 /\ bar n = 0.
+  Proof.
+    induction n ; split ; auto ;
+    destruct IHn ; auto.
+  Qed.
+
+End A.
+
+
+Module B.
+  
+  Module A := A.
+  Import A.
+
+End B.
+
+Module E.
+
+  Module B := B.
+  Import B.A.
+
+  (* Bug 1 *)
+  Lemma test_1:
+    forall (n:nat), foo n = 0.
+  Proof.
+    intros ; destruct n.
+    reflexivity.
+    specialize (A.using_foo (S n)) ; intros.
+    simpl in H.
+    simpl.
+    destruct H.
+    assumption.
+  Qed.
+
+End E.
+\ No newline at end of file