Regression test for bug #2883.

1 files changed, 34 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/2883.v b/test-suite/bugs/closed/2883.v
new file mode 100644
index 000000000..5a5d90a40
--- /dev/null
+++ b/test-suite/bugs/closed/2883.v
@@ -0,0 +1,34 @@
+Require Import List.
+Require Import Coq.Program.Equality.
+
+Inductive star {genv state : Type}
+  (step : genv -> state -> state -> Prop)
+  (ge : genv) : state -> state -> Prop :=
+  | star_refl : forall s : state, star step ge s s
+  | star_step :
+    forall (s1 : state) (s2 : state)
+      (s3 : state),
+      step ge s1 s2 ->
+      star step ge s2 s3 ->
+      star step ge s1 s3.
+
+Parameter genv expr env mem : Type.
+Definition genv' := genv.
+Inductive state : Type :=
+ | State : expr -> env -> mem -> state.
+Parameter step : genv' -> state -> state -> Prop.
+
+Section Test.
+
+Variable ge : genv'.
+
+Lemma compat_eval_steps:
+  forall a b e a' b',
+  star step ge (State a e b) (State a' e b') ->
+  True.
+Proof.
+  intros. dependent induction H.
+  trivial.
+  eapply IHstar; eauto.
+  replace s2 with (State a' e b') by admit. eauto.
+Qed. (* Oups *)