From 499a11a45b5711d4eaabe84a80f0ad3ae539d500 Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Wed, 8 May 2013 17:47:10 +0200
Subject: Imported Upstream version 8.4pl2dfsg

---
 test-suite/bugs/closed/2955.v | 52 +++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 52 insertions(+)
 create mode 100644 test-suite/bugs/closed/2955.v

(limited to 'test-suite/bugs/closed/2955.v')

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
-- 
cgit v1.2.3