Added a file for testing regression of bug #2955 (anomaly in simpl in

the presence of aliased modules). Bug was actually fixed in trunk
(thanks to PMP's monomorphization (and change of semantics) of
equality over evaluable references.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16180 85f007b7-540e-0410-9357-904b9bb8a0f7

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 000000000..45e24b5f5
--- /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