Imported Upstream version 8.2~beta3+dfsgupstream/8.2.beta3+dfsg

1 files changed, 22 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/shouldsucceed/38.v b/test-suite/bugs/closed/shouldsucceed/38.v
new file mode 100644
index 00000000..7bc04b1f
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/38.v
@@ -0,0 +1,22 @@
+Require Import Setoid.
+
+Variable A : Set.
+
+Inductive liste : Set :=
+| vide : liste
+| c : A -> liste -> liste.
+
+Inductive e : A -> liste -> Prop := 
+| ec : forall (x : A) (l : liste), e x (c x l)
+| ee : forall (x y : A) (l : liste), e x l -> e x (c y l).
+
+Definition same := fun (l m : liste) => forall (x : A), e x l <-> e x m.
+
+Definition same_refl (x:liste) : (same x x).
+  unfold same; split; intros; trivial.
+Save.
+
+Goal forall (x:liste), (same x x).
+  intro.
+  apply (same_refl x).
+Qed.