fixed bug 1791: simpl was performing eta expansion

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

1 files changed, 38 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/shouldsucceed/1791.v b/test-suite/bugs/closed/shouldsucceed/1791.v
new file mode 100644
index 000000000..694f056e8
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/1791.v
@@ -0,0 +1,38 @@
+(* simpl performs eta expansion *)
+
+Set Implicit Arguments.
+Require Import List.
+
+Definition k0 := Set.
+Definition k1 := k0 -> k0.
+
+(** iterating X n times *)
+Fixpoint Pow (X:k1)(k:nat){struct k}:k1:=
+  match k with 0 => fun X => X
+             |  S k' => fun A => X (Pow X k' A)   
+  end.
+
+Parameter Bush: k1.
+Parameter BushToList: forall (A:k0), Bush A ->  list A.
+
+Definition BushnToList (n:nat)(A:k0)(t:Pow Bush n A): list A.
+Proof.
+  intros.
+  induction n.
+  exact (t::nil).
+  simpl in t.
+  exact (flat_map IHn (BushToList t)).
+Defined.
+
+Parameter bnil : forall (A:k0), Bush A.
+Axiom BushToList_bnil: forall (A:k0), BushToList (bnil A) = nil(A:=A).
+
+Lemma BushnToList_bnil (n:nat)(A:k0):
+  BushnToList (S n) A (bnil (Pow Bush n A)) = nil.
+Proof.
+  intros.
+  simpl.
+  rewrite BushToList_bnil.
+  simpl.
+  reflexivity.
+Qed.